Proof of Theorem topdifinfeq
Step | Hyp | Ref
| Expression |
1 | | disj3 4021 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝑥) = ∅ ↔ 𝐴 = (𝐴 ∖ 𝑥)) |
2 | | eqcom 2629 |
. . . . . . . 8
⊢ (𝐴 = (𝐴 ∖ 𝑥) ↔ (𝐴 ∖ 𝑥) = 𝐴) |
3 | 1, 2 | bitri 264 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝑥) = ∅ ↔ (𝐴 ∖ 𝑥) = 𝐴) |
4 | | selpw 4165 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
5 | | sseqin2 3817 |
. . . . . . . . 9
⊢ (𝑥 ⊆ 𝐴 ↔ (𝐴 ∩ 𝑥) = 𝑥) |
6 | 4, 5 | bitri 264 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝐴 ↔ (𝐴 ∩ 𝑥) = 𝑥) |
7 | | eqeq1 2626 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝑥) = 𝑥 → ((𝐴 ∩ 𝑥) = ∅ ↔ 𝑥 = ∅)) |
8 | 6, 7 | sylbi 207 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐴 → ((𝐴 ∩ 𝑥) = ∅ ↔ 𝑥 = ∅)) |
9 | 3, 8 | syl5rbbr 275 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑥 = ∅ ↔ (𝐴 ∖ 𝑥) = 𝐴)) |
10 | | eqss 3618 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥)) |
11 | | ssdif0 3942 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝑥 ↔ (𝐴 ∖ 𝑥) = ∅) |
12 | 11 | bicomi 214 |
. . . . . . . . 9
⊢ ((𝐴 ∖ 𝑥) = ∅ ↔ 𝐴 ⊆ 𝑥) |
13 | 4, 12 | anbi12i 733 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅) ↔ (𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑥)) |
14 | 10, 13 | bitr4i 267 |
. . . . . . 7
⊢ (𝑥 = 𝐴 ↔ (𝑥 ∈ 𝒫 𝐴 ∧ (𝐴 ∖ 𝑥) = ∅)) |
15 | 14 | baib 944 |
. . . . . 6
⊢ (𝑥 ∈ 𝒫 𝐴 → (𝑥 = 𝐴 ↔ (𝐴 ∖ 𝑥) = ∅)) |
16 | 9, 15 | orbi12d 746 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝐴 → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ 𝑥) = 𝐴 ∨ (𝐴 ∖ 𝑥) = ∅))) |
17 | | orcom 402 |
. . . . 5
⊢ (((𝐴 ∖ 𝑥) = 𝐴 ∨ (𝐴 ∖ 𝑥) = ∅) ↔ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴)) |
18 | 16, 17 | syl6bb 276 |
. . . 4
⊢ (𝑥 ∈ 𝒫 𝐴 → ((𝑥 = ∅ ∨ 𝑥 = 𝐴) ↔ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))) |
19 | 18 | orbi2d 738 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝐴 → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)) ↔ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴)))) |
20 | 19 | bicomd 213 |
. 2
⊢ (𝑥 ∈ 𝒫 𝐴 → ((¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴)) ↔ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴)))) |
21 | 20 | rabbiia 3185 |
1
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ ((𝐴 ∖ 𝑥) = ∅ ∨ (𝐴 ∖ 𝑥) = 𝐴))} = {𝑥 ∈ 𝒫 𝐴 ∣ (¬ (𝐴 ∖ 𝑥) ∈ Fin ∨ (𝑥 = ∅ ∨ 𝑥 = 𝐴))} |