Proof of Theorem preimalegt
Step | Hyp | Ref
| Expression |
1 | | preimalegt.x |
. 2
⊢
Ⅎ𝑥𝜑 |
2 | | nfcv 2904 |
. . 3
⊢
Ⅎ𝑥𝐴 |
3 | | nfrab1 3296 |
. . 3
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} |
4 | 2, 3 | nfdif 4040 |
. 2
⊢
Ⅎ𝑥(𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
5 | | nfrab1 3296 |
. 2
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} |
6 | | eldifi 4041 |
. . . . 5
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → 𝑥 ∈ 𝐴) |
7 | 6 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝑥 ∈ 𝐴) |
8 | | eldifn 4042 |
. . . . . . 7
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
9 | 6 | anim1i 618 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∧ 𝐵 ≤ 𝐶) → (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
10 | | rabid 3290 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
11 | 9, 10 | sylibr 237 |
. . . . . . 7
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ∧ 𝐵 ≤ 𝐶) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
12 | 8, 11 | mtand 816 |
. . . . . 6
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) → ¬ 𝐵 ≤ 𝐶) |
13 | 12 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → ¬ 𝐵 ≤ 𝐶) |
14 | | preimalegt.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
15 | 14 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐶 ∈
ℝ*) |
16 | | preimalegt.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
17 | 6, 16 | sylan2 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐵 ∈
ℝ*) |
18 | 15, 17 | xrltnled 42575 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → (𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶)) |
19 | 13, 18 | mpbird 260 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝐶 < 𝐵) |
20 | | rabid 3290 |
. . . 4
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 < 𝐵)) |
21 | 7, 19, 20 | sylanbrc 586 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) |
22 | | rabidim1 3292 |
. . . . 5
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} → 𝑥 ∈ 𝐴) |
23 | 22 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝑥 ∈ 𝐴) |
24 | | rabidim2 42325 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵} → 𝐶 < 𝐵) |
25 | 24 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐶 < 𝐵) |
26 | 14 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐶 ∈
ℝ*) |
27 | 22, 16 | sylan2 596 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝐵 ∈
ℝ*) |
28 | 26, 27 | xrltnled 42575 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → (𝐶 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐶)) |
29 | 25, 28 | mpbid 235 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ 𝐵 ≤ 𝐶) |
30 | 29 | intnand 492 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ (𝑥 ∈ 𝐴 ∧ 𝐵 ≤ 𝐶)) |
31 | 30, 10 | sylnibr 332 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) |
32 | 23, 31 | eldifd 3877 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) → 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶})) |
33 | 21, 32 | impbida 801 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵})) |
34 | 1, 4, 5, 33 | eqrd 3920 |
1
⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐵 ≤ 𝐶}) = {𝑥 ∈ 𝐴 ∣ 𝐶 < 𝐵}) |