Proof of Theorem preimalegt
Step | Hyp | Ref
| Expression |
1 | | preimalegt.x |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → 𝑥 ∈ 𝐴) |
3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝑥 ∈ 𝐴) |
4 | 2 | anim1i 590 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∧ 𝐵 ≤ 𝐶) → (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
5 | | rabid 3095 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
6 | 4, 5 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∧ 𝐵 ≤ 𝐶) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
7 | | eldifn 3695 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
8 | 7 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∧ 𝐵 ≤ 𝐶) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
9 | 6, 8 | pm2.65da 598 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → ¬ 𝐵 ≤ 𝐶) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → ¬ 𝐵 ≤ 𝐶) |
11 | | preimalegt.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
12 | 11 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐶 ∈
ℝ*) |
13 | | preimalegt.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
14 | 3, 13 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐵 ∈
ℝ*) |
15 | 12, 14 | xrltnled 38520 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → (𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶)) |
16 | 10, 15 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐶 < 𝐵) |
17 | 3, 16 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → (𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵)) |
18 | | rabid 3095 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵)) |
19 | 17, 18 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) |
20 | 19 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) |
21 | 18 | simplbi 475 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} → 𝑥 ∈ 𝐴) |
22 | 21 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝑥 ∈ 𝐴) |
23 | 18 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} → 𝐶 < 𝐵) |
24 | 23 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐶 < 𝐵) |
25 | 11 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐶 ∈
ℝ*) |
26 | 22, 13 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐵 ∈
ℝ*) |
27 | 25, 26 | xrltnled 38520 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → (𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶)) |
28 | 24, 27 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ 𝐵 ≤ 𝐶) |
29 | 28 | intnand 953 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
30 | 29, 5 | sylnibr 318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
31 | 22, 30 | eldifd 3551 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) |
32 | 31 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} → 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}))) |
33 | 20, 32 | impbid 201 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) |
34 | 1, 33 | alrimi 2069 |
. 2
⊢ (𝜑 → ∀𝑥(𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) |
35 | | nfcv 2751 |
. . . 4
⊢
Ⅎ𝑥𝐴 |
36 | | nfrab1 3099 |
. . . 4
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} |
37 | 35, 36 | nfdif 3693 |
. . 3
⊢
Ⅎ𝑥(𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
38 | | nfrab1 3099 |
. . 3
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} |
39 | 37, 38 | dfcleqf 38281 |
. 2
⊢ ((𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) |
40 | 34, 39 | sylibr 223 |
1
⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) |