# 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 syl5bi ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( ( 𝐴𝑥 ) ≼ ω ∨ 𝑥 = ∅ ) } → ( ¬ 𝑦 = ∅ → ( 𝐴 𝑦 ) ≼ ω ) )
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 ‘ 𝐴 ) )