Step | Hyp | Ref
| Expression |
1 | | uniss 4458 |
. . . . . . . 8
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
2 | | ssrab2 3687 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 |
3 | | sspwuni 4611 |
. . . . . . . . 9
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 ↔ ∪ {𝑥
∈ 𝒫 𝐴 ∣
((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴) |
4 | 2, 3 | mpbi 220 |
. . . . . . . 8
⊢ ∪ {𝑥
∈ 𝒫 𝐴 ∣
((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴 |
5 | 1, 4 | syl6ss 3615 |
. . . . . . 7
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
⊆ 𝐴) |
6 | | vuniex 6954 |
. . . . . . . 8
⊢ ∪ 𝑦
∈ V |
7 | 6 | elpw 4164 |
. . . . . . 7
⊢ (∪ 𝑦
∈ 𝒫 𝐴 ↔
∪ 𝑦 ⊆ 𝐴) |
8 | 5, 7 | sylibr 224 |
. . . . . 6
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ 𝒫 𝐴) |
9 | | uni0c 4464 |
. . . . . . . . . . 11
⊢ (∪ 𝑦 =
∅ ↔ ∀𝑧
∈ 𝑦 𝑧 = ∅) |
10 | 9 | notbii 310 |
. . . . . . . . . 10
⊢ (¬
∪ 𝑦 = ∅ ↔ ¬ ∀𝑧 ∈ 𝑦 𝑧 = ∅) |
11 | | rexnal 2995 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑦 ¬ 𝑧 = ∅ ↔ ¬ ∀𝑧 ∈ 𝑦 𝑧 = ∅) |
12 | 10, 11 | bitr4i 267 |
. . . . . . . . 9
⊢ (¬
∪ 𝑦 = ∅ ↔ ∃𝑧 ∈ 𝑦 ¬ 𝑧 = ∅) |
13 | | ssel2 3598 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
14 | | difeq2 3722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑧)) |
15 | 14 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ 𝑧) ∈ Fin)) |
16 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅)) |
17 | 15, 16 | orbi12d 746 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑧 → (((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) |
18 | 17 | elrab 3363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) |
19 | 13, 18 | sylib 208 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) |
20 | 19 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅)) |
21 | 20 | ord 392 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (¬ (𝐴 ∖ 𝑧) ∈ Fin → 𝑧 = ∅)) |
22 | 21 | con1d 139 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 = ∅ → (𝐴 ∖ 𝑧) ∈ Fin)) |
23 | 22 | imp 445 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴 ∖ 𝑧) ∈ Fin) |
24 | | elssuni 4467 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦) |
25 | 24 | sscond 3747 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝑦 → (𝐴 ∖ ∪ 𝑦) ⊆ (𝐴 ∖ 𝑧)) |
26 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∖ 𝑧) ∈ Fin ∧ (𝐴 ∖ ∪ 𝑦) ⊆ (𝐴 ∖ 𝑧)) → (𝐴 ∖ ∪ 𝑦) ∈ Fin) |
27 | 25, 26 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∖ 𝑧) ∈ Fin ∧ 𝑧 ∈ 𝑦) → (𝐴 ∖ ∪ 𝑦) ∈ Fin) |
28 | 27 | expcom 451 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝑦 → ((𝐴 ∖ 𝑧) ∈ Fin → (𝐴 ∖ ∪ 𝑦) ∈ Fin)) |
29 | 28 | ad2antlr 763 |
. . . . . . . . . . . 12
⊢ (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) → ((𝐴 ∖ 𝑧) ∈ Fin → (𝐴 ∖ ∪ 𝑦) ∈ Fin)) |
30 | 23, 29 | mpd 15 |
. . . . . . . . . . 11
⊢ (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴 ∖ ∪ 𝑦) ∈ Fin) |
31 | 30 | exp31 630 |
. . . . . . . . . 10
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (𝑧 ∈ 𝑦 → (¬ 𝑧 = ∅ → (𝐴 ∖ ∪ 𝑦) ∈ Fin))) |
32 | 31 | rexlimdv 3030 |
. . . . . . . . 9
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (∃𝑧 ∈ 𝑦 ¬ 𝑧 = ∅ → (𝐴 ∖ ∪ 𝑦) ∈ Fin)) |
33 | 12, 32 | syl5bi 232 |
. . . . . . . 8
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (¬ ∪ 𝑦 =
∅ → (𝐴 ∖
∪ 𝑦) ∈ Fin)) |
34 | 33 | con1d 139 |
. . . . . . 7
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (¬ (𝐴 ∖ ∪ 𝑦) ∈ Fin → ∪ 𝑦 =
∅)) |
35 | 34 | orrd 393 |
. . . . . 6
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ((𝐴 ∖ ∪ 𝑦) ∈ Fin ∨ ∪ 𝑦 =
∅)) |
36 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = ∪
𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ ∪ 𝑦)) |
37 | 36 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝑦 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ ∪ 𝑦) ∈ Fin)) |
38 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = ∪
𝑦 → (𝑥 = ∅ ↔ ∪ 𝑦 =
∅)) |
39 | 37, 38 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = ∪
𝑦 → (((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ ∪ 𝑦) ∈ Fin ∨ ∪ 𝑦 =
∅))) |
40 | 39 | elrab 3363 |
. . . . . 6
⊢ (∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (∪ 𝑦
∈ 𝒫 𝐴 ∧
((𝐴 ∖ ∪ 𝑦)
∈ Fin ∨ ∪ 𝑦 = ∅))) |
41 | 8, 35, 40 | sylanbrc 698 |
. . . . 5
⊢ (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
42 | 41 | ax-gen 1722 |
. . . 4
⊢
∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
43 | | ssinss1 3841 |
. . . . . . . . 9
⊢ (𝑦 ⊆ 𝐴 → (𝑦 ∩ 𝑧) ⊆ 𝐴) |
44 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
45 | 44 | elpw 4164 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴) |
46 | 44 | inex1 4799 |
. . . . . . . . . 10
⊢ (𝑦 ∩ 𝑧) ∈ V |
47 | 46 | elpw 4164 |
. . . . . . . . 9
⊢ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ↔ (𝑦 ∩ 𝑧) ⊆ 𝐴) |
48 | 43, 45, 47 | 3imtr4i 281 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝒫 𝐴 → (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴) |
49 | 48 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) → (𝑦 ∩ 𝑧) ∈ 𝒫 𝐴) |
50 | | difindi 3881 |
. . . . . . . . . . 11
⊢ (𝐴 ∖ (𝑦 ∩ 𝑧)) = ((𝐴 ∖ 𝑦) ∪ (𝐴 ∖ 𝑧)) |
51 | | unfi 8227 |
. . . . . . . . . . 11
⊢ (((𝐴 ∖ 𝑦) ∈ Fin ∧ (𝐴 ∖ 𝑧) ∈ Fin) → ((𝐴 ∖ 𝑦) ∪ (𝐴 ∖ 𝑧)) ∈ Fin) |
52 | 50, 51 | syl5eqel 2705 |
. . . . . . . . . 10
⊢ (((𝐴 ∖ 𝑦) ∈ Fin ∧ (𝐴 ∖ 𝑧) ∈ Fin) → (𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin) |
53 | 52 | orcd 407 |
. . . . . . . . 9
⊢ (((𝐴 ∖ 𝑦) ∈ Fin ∧ (𝐴 ∖ 𝑧) ∈ Fin) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅)) |
54 | | ineq1 3807 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝑦 ∩ 𝑧) = (∅ ∩ 𝑧)) |
55 | | 0in 3969 |
. . . . . . . . . . 11
⊢ (∅
∩ 𝑧) =
∅ |
56 | 54, 55 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → (𝑦 ∩ 𝑧) = ∅) |
57 | 56 | olcd 408 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅)) |
58 | | ineq2 3808 |
. . . . . . . . . . 11
⊢ (𝑧 = ∅ → (𝑦 ∩ 𝑧) = (𝑦 ∩ ∅)) |
59 | | in0 3968 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ ∅) =
∅ |
60 | 58, 59 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝑧 = ∅ → (𝑦 ∩ 𝑧) = ∅) |
61 | 60 | olcd 408 |
. . . . . . . . 9
⊢ (𝑧 = ∅ → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅)) |
62 | 53, 57, 61 | ccase2 989 |
. . . . . . . 8
⊢ ((((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅) ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅)) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅)) |
63 | 62 | ad2ant2l 782 |
. . . . . . 7
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) → ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅)) |
64 | 49, 63 | jca 554 |
. . . . . 6
⊢ (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅))) → ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅))) |
65 | | difeq2 3722 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝑦)) |
66 | 65 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ 𝑦) ∈ Fin)) |
67 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅)) |
68 | 66, 67 | orbi12d 746 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅))) |
69 | 68 | elrab 3363 |
. . . . . . 7
⊢ (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅))) |
70 | 69, 18 | anbi12i 733 |
. . . . . 6
⊢ ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ 𝑧) ∈ Fin ∨ 𝑧 = ∅)))) |
71 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝐴 ∖ 𝑥) = (𝐴 ∖ (𝑦 ∩ 𝑧))) |
72 | 71 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → ((𝐴 ∖ 𝑥) ∈ Fin ↔ (𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin)) |
73 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (𝑥 = ∅ ↔ (𝑦 ∩ 𝑧) = ∅)) |
74 | 72, 73 | orbi12d 746 |
. . . . . . 7
⊢ (𝑥 = (𝑦 ∩ 𝑧) → (((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅))) |
75 | 74 | elrab 3363 |
. . . . . 6
⊢ ((𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ ((𝑦 ∩ 𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦 ∩ 𝑧)) ∈ Fin ∨ (𝑦 ∩ 𝑧) = ∅))) |
76 | 64, 70, 75 | 3imtr4i 281 |
. . . . 5
⊢ ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) → (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
77 | 76 | rgen2a 2977 |
. . . 4
⊢
∀𝑦 ∈
{𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} |
78 | 42, 77 | pm3.2i 471 |
. . 3
⊢
(∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
79 | | pwexg 4850 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) |
80 | | rabexg 4812 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → {𝑥 ∈
𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ V) |
81 | | istopg 20700 |
. . . 4
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}))) |
82 | 79, 80, 81 | 3syl 18 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ∪ 𝑦
∈ {𝑥 ∈ 𝒫
𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦 ∩ 𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}))) |
83 | 78, 82 | mpbiri 248 |
. 2
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top) |
84 | | pwidg 4173 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴) |
85 | | 0fin 8188 |
. . . . . . 7
⊢ ∅
∈ Fin |
86 | 85 | orci 405 |
. . . . . 6
⊢ (∅
∈ Fin ∨ 𝐴 =
∅) |
87 | 86 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∅ ∈ Fin ∨ 𝐴 = ∅)) |
88 | | difeq2 3722 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = (𝐴 ∖ 𝐴)) |
89 | | difid 3948 |
. . . . . . . . 9
⊢ (𝐴 ∖ 𝐴) = ∅ |
90 | 88, 89 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝐴 ∖ 𝑥) = ∅) |
91 | 90 | eleq1d 2686 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝐴 ∖ 𝑥) ∈ Fin ↔ ∅ ∈
Fin)) |
92 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅)) |
93 | 91, 92 | orbi12d 746 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ (∅ ∈ Fin ∨
𝐴 =
∅))) |
94 | 93 | elrab 3363 |
. . . . 5
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝐴 ∈ 𝒫 𝐴 ∧ (∅ ∈ Fin ∨ 𝐴 = ∅))) |
95 | 84, 87, 94 | sylanbrc 698 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
96 | | elssuni 4467 |
. . . 4
⊢ (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
97 | 95, 96 | syl 17 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
98 | 4 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴) |
99 | 97, 98 | eqssd 3620 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 = ∪ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)}) |
100 | | istopon 20717 |
. 2
⊢ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ∧ 𝐴 = ∪
{𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)})) |
101 | 83, 99, 100 | sylanbrc 698 |
1
⊢ (𝐴 ∈ 𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴 ∖ 𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴)) |