MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fctop Structured version   Visualization version   GIF version

Theorem fctop 20789
Description: The finite complement topology on a set 𝐴. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.) (Revised by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
fctop (𝐴𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝑉(𝑥)

Proof of Theorem fctop
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniss 4449 . . . . . . . 8 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
2 ssrab2 3679 . . . . . . . . 9 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴
3 sspwuni 4602 . . . . . . . . 9 ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝒫 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴)
42, 3mpbi 220 . . . . . . . 8 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴
51, 4syl6ss 3607 . . . . . . 7 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦𝐴)
6 vuniex 6939 . . . . . . . 8 𝑦 ∈ V
76elpw 4155 . . . . . . 7 ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴)
85, 7sylibr 224 . . . . . 6 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ 𝒫 𝐴)
9 uni0c 4455 . . . . . . . . . . 11 ( 𝑦 = ∅ ↔ ∀𝑧𝑦 𝑧 = ∅)
109notbii 310 . . . . . . . . . 10 𝑦 = ∅ ↔ ¬ ∀𝑧𝑦 𝑧 = ∅)
11 rexnal 2992 . . . . . . . . . 10 (∃𝑧𝑦 ¬ 𝑧 = ∅ ↔ ¬ ∀𝑧𝑦 𝑧 = ∅)
1210, 11bitr4i 267 . . . . . . . . 9 𝑦 = ∅ ↔ ∃𝑧𝑦 ¬ 𝑧 = ∅)
13 ssel2 3590 . . . . . . . . . . . . . . . . 17 ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) → 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
14 difeq2 3714 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑧 → (𝐴𝑥) = (𝐴𝑧))
1514eleq1d 2684 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑧) ∈ Fin))
16 eqeq1 2624 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅))
1715, 16orbi12d 745 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑧 → (((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅)))
1817elrab 3357 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅)))
1913, 18sylib 208 . . . . . . . . . . . . . . . 16 ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) → (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅)))
2019simprd 479 . . . . . . . . . . . . . . 15 ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) → ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅))
2120ord 392 . . . . . . . . . . . . . 14 ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) → (¬ (𝐴𝑧) ∈ Fin → 𝑧 = ∅))
2221con1d 139 . . . . . . . . . . . . 13 ((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) → (¬ 𝑧 = ∅ → (𝐴𝑧) ∈ Fin))
2322imp 445 . . . . . . . . . . . 12 (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴𝑧) ∈ Fin)
24 elssuni 4458 . . . . . . . . . . . . . . . 16 (𝑧𝑦𝑧 𝑦)
2524sscond 3739 . . . . . . . . . . . . . . 15 (𝑧𝑦 → (𝐴 𝑦) ⊆ (𝐴𝑧))
26 ssfi 8165 . . . . . . . . . . . . . . 15 (((𝐴𝑧) ∈ Fin ∧ (𝐴 𝑦) ⊆ (𝐴𝑧)) → (𝐴 𝑦) ∈ Fin)
2725, 26sylan2 491 . . . . . . . . . . . . . 14 (((𝐴𝑧) ∈ Fin ∧ 𝑧𝑦) → (𝐴 𝑦) ∈ Fin)
2827expcom 451 . . . . . . . . . . . . 13 (𝑧𝑦 → ((𝐴𝑧) ∈ Fin → (𝐴 𝑦) ∈ Fin))
2928ad2antlr 762 . . . . . . . . . . . 12 (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) ∧ ¬ 𝑧 = ∅) → ((𝐴𝑧) ∈ Fin → (𝐴 𝑦) ∈ Fin))
3023, 29mpd 15 . . . . . . . . . . 11 (((𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧𝑦) ∧ ¬ 𝑧 = ∅) → (𝐴 𝑦) ∈ Fin)
3130exp31 629 . . . . . . . . . 10 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (𝑧𝑦 → (¬ 𝑧 = ∅ → (𝐴 𝑦) ∈ Fin)))
3231rexlimdv 3026 . . . . . . . . 9 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (∃𝑧𝑦 ¬ 𝑧 = ∅ → (𝐴 𝑦) ∈ Fin))
3312, 32syl5bi 232 . . . . . . . 8 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (¬ 𝑦 = ∅ → (𝐴 𝑦) ∈ Fin))
3433con1d 139 . . . . . . 7 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → (¬ (𝐴 𝑦) ∈ Fin → 𝑦 = ∅))
3534orrd 393 . . . . . 6 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → ((𝐴 𝑦) ∈ Fin ∨ 𝑦 = ∅))
36 difeq2 3714 . . . . . . . . 9 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴 𝑦))
3736eleq1d 2684 . . . . . . . 8 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴 𝑦) ∈ Fin))
38 eqeq1 2624 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
3937, 38orbi12d 745 . . . . . . 7 (𝑥 = 𝑦 → (((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 𝑦) ∈ Fin ∨ 𝑦 = ∅)))
4039elrab 3357 . . . . . 6 ( 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴 𝑦) ∈ Fin ∨ 𝑦 = ∅)))
418, 35, 40sylanbrc 697 . . . . 5 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
4241ax-gen 1720 . . . 4 𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
43 ssinss1 3833 . . . . . . . . 9 (𝑦𝐴 → (𝑦𝑧) ⊆ 𝐴)
44 vex 3198 . . . . . . . . . 10 𝑦 ∈ V
4544elpw 4155 . . . . . . . . 9 (𝑦 ∈ 𝒫 𝐴𝑦𝐴)
4644inex1 4790 . . . . . . . . . 10 (𝑦𝑧) ∈ V
4746elpw 4155 . . . . . . . . 9 ((𝑦𝑧) ∈ 𝒫 𝐴 ↔ (𝑦𝑧) ⊆ 𝐴)
4843, 45, 473imtr4i 281 . . . . . . . 8 (𝑦 ∈ 𝒫 𝐴 → (𝑦𝑧) ∈ 𝒫 𝐴)
4948ad2antrr 761 . . . . . . 7 (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅))) → (𝑦𝑧) ∈ 𝒫 𝐴)
50 difindi 3873 . . . . . . . . . . 11 (𝐴 ∖ (𝑦𝑧)) = ((𝐴𝑦) ∪ (𝐴𝑧))
51 unfi 8212 . . . . . . . . . . 11 (((𝐴𝑦) ∈ Fin ∧ (𝐴𝑧) ∈ Fin) → ((𝐴𝑦) ∪ (𝐴𝑧)) ∈ Fin)
5250, 51syl5eqel 2703 . . . . . . . . . 10 (((𝐴𝑦) ∈ Fin ∧ (𝐴𝑧) ∈ Fin) → (𝐴 ∖ (𝑦𝑧)) ∈ Fin)
5352orcd 407 . . . . . . . . 9 (((𝐴𝑦) ∈ Fin ∧ (𝐴𝑧) ∈ Fin) → ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅))
54 ineq1 3799 . . . . . . . . . . 11 (𝑦 = ∅ → (𝑦𝑧) = (∅ ∩ 𝑧))
55 0in 3960 . . . . . . . . . . 11 (∅ ∩ 𝑧) = ∅
5654, 55syl6eq 2670 . . . . . . . . . 10 (𝑦 = ∅ → (𝑦𝑧) = ∅)
5756olcd 408 . . . . . . . . 9 (𝑦 = ∅ → ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅))
58 ineq2 3800 . . . . . . . . . . 11 (𝑧 = ∅ → (𝑦𝑧) = (𝑦 ∩ ∅))
59 in0 3959 . . . . . . . . . . 11 (𝑦 ∩ ∅) = ∅
6058, 59syl6eq 2670 . . . . . . . . . 10 (𝑧 = ∅ → (𝑦𝑧) = ∅)
6160olcd 408 . . . . . . . . 9 (𝑧 = ∅ → ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅))
6253, 57, 61ccase2 988 . . . . . . . 8 ((((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅) ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅)) → ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅))
6362ad2ant2l 781 . . . . . . 7 (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅))) → ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅))
6449, 63jca 554 . . . . . 6 (((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅))) → ((𝑦𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅)))
65 difeq2 3714 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝐴𝑥) = (𝐴𝑦))
6665eleq1d 2684 . . . . . . . . 9 (𝑥 = 𝑦 → ((𝐴𝑥) ∈ Fin ↔ (𝐴𝑦) ∈ Fin))
67 eqeq1 2624 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
6866, 67orbi12d 745 . . . . . . . 8 (𝑥 = 𝑦 → (((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)))
6968elrab 3357 . . . . . . 7 (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)))
7069, 18anbi12i 732 . . . . . 6 ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ ((𝐴𝑦) ∈ Fin ∨ 𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ ((𝐴𝑧) ∈ Fin ∨ 𝑧 = ∅))))
71 difeq2 3714 . . . . . . . . 9 (𝑥 = (𝑦𝑧) → (𝐴𝑥) = (𝐴 ∖ (𝑦𝑧)))
7271eleq1d 2684 . . . . . . . 8 (𝑥 = (𝑦𝑧) → ((𝐴𝑥) ∈ Fin ↔ (𝐴 ∖ (𝑦𝑧)) ∈ Fin))
73 eqeq1 2624 . . . . . . . 8 (𝑥 = (𝑦𝑧) → (𝑥 = ∅ ↔ (𝑦𝑧) = ∅))
7472, 73orbi12d 745 . . . . . . 7 (𝑥 = (𝑦𝑧) → (((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅)))
7574elrab 3357 . . . . . 6 ((𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ ((𝑦𝑧) ∈ 𝒫 𝐴 ∧ ((𝐴 ∖ (𝑦𝑧)) ∈ Fin ∨ (𝑦𝑧) = ∅)))
7664, 70, 753imtr4i 281 . . . . 5 ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
7776rgen2a 2974 . . . 4 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}
7842, 77pm3.2i 471 . . 3 (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
79 pwexg 4841 . . . 4 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
80 rabexg 4803 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ V)
81 istopg 20681 . . . 4 ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})))
8279, 80, 813syl 18 . . 3 (𝐴𝑉 → ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})))
8378, 82mpbiri 248 . 2 (𝐴𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top)
84 pwidg 4164 . . . . 5 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
85 0fin 8173 . . . . . . 7 ∅ ∈ Fin
8685orci 405 . . . . . 6 (∅ ∈ Fin ∨ 𝐴 = ∅)
8786a1i 11 . . . . 5 (𝐴𝑉 → (∅ ∈ Fin ∨ 𝐴 = ∅))
88 difeq2 3714 . . . . . . . . 9 (𝑥 = 𝐴 → (𝐴𝑥) = (𝐴𝐴))
89 difid 3939 . . . . . . . . 9 (𝐴𝐴) = ∅
9088, 89syl6eq 2670 . . . . . . . 8 (𝑥 = 𝐴 → (𝐴𝑥) = ∅)
9190eleq1d 2684 . . . . . . 7 (𝑥 = 𝐴 → ((𝐴𝑥) ∈ Fin ↔ ∅ ∈ Fin))
92 eqeq1 2624 . . . . . . 7 (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅))
9391, 92orbi12d 745 . . . . . 6 (𝑥 = 𝐴 → (((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅) ↔ (∅ ∈ Fin ∨ 𝐴 = ∅)))
9493elrab 3357 . . . . 5 (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ↔ (𝐴 ∈ 𝒫 𝐴 ∧ (∅ ∈ Fin ∨ 𝐴 = ∅)))
9584, 87, 94sylanbrc 697 . . . 4 (𝐴𝑉𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
96 elssuni 4458 . . . 4 (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
9795, 96syl 17 . . 3 (𝐴𝑉𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
984a1i 11 . . 3 (𝐴𝑉 {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ⊆ 𝐴)
9997, 98eqssd 3612 . 2 (𝐴𝑉𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)})
100 istopon 20698 . 2 ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ Top ∧ 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)}))
10183, 99, 100sylanbrc 697 1 (𝐴𝑉 → {𝑥 ∈ 𝒫 𝐴 ∣ ((𝐴𝑥) ∈ Fin ∨ 𝑥 = ∅)} ∈ (TopOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  wal 1479   = wceq 1481  wcel 1988  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  𝒫 cpw 4149   cuni 4427  cfv 5876  Fincfn 7940  Topctop 20679  TopOnctopon 20696
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-oadd 7549  df-er 7727  df-en 7941  df-fin 7944  df-top 20680  df-topon 20697
This theorem is referenced by:  fctop2  20790
  Copyright terms: Public domain W3C validator