This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fctop

Description: The finite complement topology on a set A . Example 3 in Munkres p. 77. (Contributed by FL, 15-Aug-2006) (Revised by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion fctop ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 difeq2 ⊢ ( 𝑥 = ∪ 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ∪ 𝑦 ) )
2 1 eleq1d ⊢ ( 𝑥 = ∪ 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ) )
3 eqeq1 ⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑥 = ∅ ↔ ∪ 𝑦 = ∅ ) )
4 2 3 orbi12d ⊢ ( 𝑥 = ∪ 𝑦 → ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ∨ ∪ 𝑦 = ∅ ) ) )
5 uniss ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ⊆ ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
6 ssrab2 ⊢ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ⊆ 𝒫 𝐴
7 sspwuni ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ⊆ 𝒫 𝐴 ↔ ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ⊆ 𝐴 )
8 6 7 mpbi ⊢ ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ⊆ 𝐴
9 5 8 sstrdi ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ⊆ 𝐴 )
10 vuniex ⊢ ∪ 𝑦 ∈ V
11 10 elpw ⊢ ( ∪ 𝑦 ∈ 𝒫 𝐴 ↔ ∪ 𝑦 ⊆ 𝐴 )
12 9 11 sylibr ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ 𝒫 𝐴 )
13 uni0c ⊢ ( ∪ 𝑦 = ∅ ↔ ∀ 𝑧 ∈ 𝑦 𝑧 = ∅ )
14 13 notbii ⊢ ( ¬ ∪ 𝑦 = ∅ ↔ ¬ ∀ 𝑧 ∈ 𝑦 𝑧 = ∅ )
15 rexnal ⊢ ( ∃ 𝑧 ∈ 𝑦 ¬ 𝑧 = ∅ ↔ ¬ ∀ 𝑧 ∈ 𝑦 𝑧 = ∅ )
16 14 15 bitr4i ⊢ ( ¬ ∪ 𝑦 = ∅ ↔ ∃ 𝑧 ∈ 𝑦 ¬ 𝑧 = ∅ )
17 ssel2 ⊢ ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
18 difeq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑧 ) )
19 18 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑧 ) ∈ Fin ) )
20 eqeq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 = ∅ ↔ 𝑧 = ∅ ) )
21 19 20 orbi12d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) )
22 21 elrab ⊢ ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) )
23 17 22 sylib ⊢ ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) → ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) )
24 23 simprd ⊢ ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) → ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) )
25 24 ord ⊢ ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) → ( ¬ ( 𝐴 ∖ 𝑧 ) ∈ Fin → 𝑧 = ∅ ) )
26 25 con1d ⊢ ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) → ( ¬ 𝑧 = ∅ → ( 𝐴 ∖ 𝑧 ) ∈ Fin ) )
27 26 imp ⊢ ( ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) ∧ ¬ 𝑧 = ∅ ) → ( 𝐴 ∖ 𝑧 ) ∈ Fin )
28 elssuni ⊢ ( 𝑧 ∈ 𝑦 → 𝑧 ⊆ ∪ 𝑦 )
29 28 sscond ⊢ ( 𝑧 ∈ 𝑦 → ( 𝐴 ∖ ∪ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑧 ) )
30 ssfi ⊢ ( ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ ( 𝐴 ∖ ∪ 𝑦 ) ⊆ ( 𝐴 ∖ 𝑧 ) ) → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin )
31 29 30 sylan2 ⊢ ( ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∧ 𝑧 ∈ 𝑦 ) → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin )
32 31 expcom ⊢ ( 𝑧 ∈ 𝑦 → ( ( 𝐴 ∖ 𝑧 ) ∈ Fin → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ) )
33 32 ad2antlr ⊢ ( ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) ∧ ¬ 𝑧 = ∅ ) → ( ( 𝐴 ∖ 𝑧 ) ∈ Fin → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ) )
34 27 33 mpd ⊢ ( ( ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ 𝑦 ) ∧ ¬ 𝑧 = ∅ ) → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin )
35 34 rexlimdva2 ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ( ∃ 𝑧 ∈ 𝑦 ¬ 𝑧 = ∅ → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ) )
36 16 35 biimtrid ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ( ¬ ∪ 𝑦 = ∅ → ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ) )
37 36 con1d ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ( ¬ ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin → ∪ 𝑦 = ∅ ) )
38 37 orrd ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ( ( 𝐴 ∖ ∪ 𝑦 ) ∈ Fin ∨ ∪ 𝑦 = ∅ ) )
39 4 12 38 elrabd ⊢ ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
40 39 ax-gen ⊢ ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
41 ssinss1 ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 )
42 vex ⊢ 𝑦 ∈ V
43 42 elpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
44 42 inex1 ⊢ ( 𝑦 ∩ 𝑧 ) ∈ V
45 44 elpw ⊢ ( ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝐴 ↔ ( 𝑦 ∩ 𝑧 ) ⊆ 𝐴 )
46 41 43 45 3imtr4i ⊢ ( 𝑦 ∈ 𝒫 𝐴 → ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝐴 )
47 46 ad2antrr ⊢ ( ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) ) → ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝐴 )
48 difindi ⊢ ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) = ( ( 𝐴 ∖ 𝑦 ) ∪ ( 𝐴 ∖ 𝑧 ) )
49 unfi ⊢ ( ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑧 ) ∈ Fin ) → ( ( 𝐴 ∖ 𝑦 ) ∪ ( 𝐴 ∖ 𝑧 ) ) ∈ Fin )
50 48 49 eqeltrid ⊢ ( ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑧 ) ∈ Fin ) → ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin )
51 50 orcd ⊢ ( ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∧ ( 𝐴 ∖ 𝑧 ) ∈ Fin ) → ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
52 ineq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∩ 𝑧 ) = ( ∅ ∩ 𝑧 ) )
53 0in ⊢ ( ∅ ∩ 𝑧 ) = ∅
54 52 53 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑦 ∩ 𝑧 ) = ∅ )
55 54 olcd ⊢ ( 𝑦 = ∅ → ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
56 ineq2 ⊢ ( 𝑧 = ∅ → ( 𝑦 ∩ 𝑧 ) = ( 𝑦 ∩ ∅ ) )
57 in0 ⊢ ( 𝑦 ∩ ∅ ) = ∅
58 56 57 eqtrdi ⊢ ( 𝑧 = ∅ → ( 𝑦 ∩ 𝑧 ) = ∅ )
59 58 olcd ⊢ ( 𝑧 = ∅ → ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
60 51 55 59 ccase2 ⊢ ( ( ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) → ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
61 60 ad2ant2l ⊢ ( ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) ) → ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
62 47 61 jca ⊢ ( ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) ) → ( ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) ) )
63 difeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
64 63 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ 𝑦 ) ∈ Fin ) )
65 eqeq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
66 64 65 orbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) )
67 66 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) )
68 67 22 anbi12i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ↔ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑦 ) ∈ Fin ∨ 𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ 𝑧 ) ∈ Fin ∨ 𝑧 = ∅ ) ) ) )
69 difeq2 ⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) )
70 69 eleq1d ⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ) )
71 eqeq1 ⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( 𝑥 = ∅ ↔ ( 𝑦 ∩ 𝑧 ) = ∅ ) )
72 70 71 orbi12d ⊢ ( 𝑥 = ( 𝑦 ∩ 𝑧 ) → ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) ) )
73 72 elrab ⊢ ( ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ↔ ( ( 𝑦 ∩ 𝑧 ) ∈ 𝒫 𝐴 ∧ ( ( 𝐴 ∖ ( 𝑦 ∩ 𝑧 ) ) ∈ Fin ∨ ( 𝑦 ∩ 𝑧 ) = ∅ ) ) )
74 62 68 73 3imtr4i ⊢ ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) → ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
75 74 rgen2 ⊢ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) }
76 40 75 pm3.2i ⊢ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
77 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
78 rabexg ⊢ ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ V )
79 istopg ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ V → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ) )
80 77 78 79 3syl ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ( 𝑦 ∩ 𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) ) )
81 76 80 mpbiri ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ Top )
82 difeq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝐴 ) )
83 difid ⊢ ( 𝐴 ∖ 𝐴 ) = ∅
84 82 83 eqtrdi ⊢ ( 𝑥 = 𝐴 → ( 𝐴 ∖ 𝑥 ) = ∅ )
85 84 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ↔ ∅ ∈ Fin ) )
86 eqeq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 = ∅ ↔ 𝐴 = ∅ ) )
87 85 86 orbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) ↔ ( ∅ ∈ Fin ∨ 𝐴 = ∅ ) ) )
88 pwidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝒫 𝐴 )
89 0fi ⊢ ∅ ∈ Fin
90 89 orci ⊢ ( ∅ ∈ Fin ∨ 𝐴 = ∅ )
91 90 a1i ⊢ ( 𝐴 ∈ 𝑉 → ( ∅ ∈ Fin ∨ 𝐴 = ∅ ) )
92 87 88 91 elrabd ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
93 elssuni ⊢ ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } → 𝐴 ⊆ ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
94 92 93 syl ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
95 8 a1i ⊢ ( 𝐴 ∈ 𝑉 → ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ⊆ 𝐴 )
96 94 95 eqssd ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 = ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } )
97 istopon ⊢ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) ↔ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ Top ∧ 𝐴 = ∪ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ) )
98 81 96 97 sylanbrc ⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴 ∖ 𝑥 ) ∈ Fin ∨ 𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )