Metamath Proof Explorer

Theorem cctop

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

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

Proof

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