Proof of Theorem preimagelt
Step | Hyp | Ref
| Expression |
1 | | preimagelt.x |
. . 3
⊢
Ⅎ𝑥𝜑 |
2 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) → 𝑥 ∈ 𝐴) |
3 | 2 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → 𝑥 ∈ 𝐴) |
4 | 2 | anim1i 592 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ∧ 𝐶 ≤ 𝐵) → (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵)) |
5 | | rabid 3116 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} ↔ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵)) |
6 | 4, 5 | sylibr 224 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ∧ 𝐶 ≤ 𝐵) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
7 | | eldifn 3733 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
8 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ∧ 𝐶 ≤ 𝐵) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
9 | 6, 8 | pm2.65da 600 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) → ¬ 𝐶 ≤ 𝐵) |
10 | 9 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → ¬ 𝐶 ≤ 𝐵) |
11 | | preimagelt.b |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
12 | 3, 11 | syldan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → 𝐵 ∈
ℝ*) |
13 | | preimagelt.c |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
14 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → 𝐶 ∈
ℝ*) |
15 | 12, 14 | xrltnled 39579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → (𝐵 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐵)) |
16 | 10, 15 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → 𝐵 < 𝐶) |
17 | 3, 16 | jca 554 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → (𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶)) |
18 | | rabid 3116 |
. . . . . 6
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 < 𝐶)) |
19 | 17, 18 | sylibr 224 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) |
20 | 19 | ex 450 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) → 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶})) |
21 | 18 | simplbi 476 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} → 𝑥 ∈ 𝐴) |
22 | 21 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → 𝑥 ∈ 𝐴) |
23 | 18 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} → 𝐵 < 𝐶) |
24 | 23 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → 𝐵 < 𝐶) |
25 | 22, 11 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → 𝐵 ∈
ℝ*) |
26 | 13 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → 𝐶 ∈
ℝ*) |
27 | 25, 26 | xrltnled 39579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → (𝐵 < 𝐶 ↔ ¬ 𝐶 ≤ 𝐵)) |
28 | 24, 27 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → ¬ 𝐶 ≤ 𝐵) |
29 | 28 | intnand 962 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → ¬ (𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝐵)) |
30 | 29, 5 | sylnibr 319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → ¬ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
31 | 22, 30 | eldifd 3585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) → 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵})) |
32 | 31 | ex 450 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} → 𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}))) |
33 | 20, 32 | impbid 202 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶})) |
34 | 1, 33 | alrimi 2082 |
. 2
⊢ (𝜑 → ∀𝑥(𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶})) |
35 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑥𝐴 |
36 | | nfrab1 3122 |
. . . 4
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵} |
37 | 35, 36 | nfdif 3731 |
. . 3
⊢
Ⅎ𝑥(𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) |
38 | | nfrab1 3122 |
. . 3
⊢
Ⅎ𝑥{𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} |
39 | 37, 38 | dfcleqf 39255 |
. 2
⊢ ((𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) = {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶} ↔ ∀𝑥(𝑥 ∈ (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) ↔ 𝑥 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶})) |
40 | 34, 39 | sylibr 224 |
1
⊢ (𝜑 → (𝐴 ∖ {𝑥 ∈ 𝐴 ∣ 𝐶 ≤ 𝐵}) = {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝐶}) |