# 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 syl5bi ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴𝑥 ) ∈ 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 0fin ∅ ∈ 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 ‘ 𝐴 ) )