# Metamath Proof Explorer

## Theorem ppttop

Description: The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion ppttop ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 ssrab ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ↔ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) )
2 eleq2 ( 𝑥 = 𝑦 → ( 𝑃𝑥𝑃 𝑦 ) )
3 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
4 2 3 orbi12d ( 𝑥 = 𝑦 → ( ( 𝑃𝑥𝑥 = ∅ ) ↔ ( 𝑃 𝑦 𝑦 = ∅ ) ) )
5 simprl ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → 𝑦 ⊆ 𝒫 𝐴 )
6 sspwuni ( 𝑦 ⊆ 𝒫 𝐴 𝑦𝐴 )
7 5 6 sylib ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → 𝑦𝐴 )
8 vuniex 𝑦 ∈ V
9 8 elpw ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴 )
10 7 9 sylibr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → 𝑦 ∈ 𝒫 𝐴 )
11 neq0 ( ¬ 𝑦 = ∅ ↔ ∃ 𝑧 𝑧 𝑦 )
12 eluni2 ( 𝑧 𝑦 ↔ ∃ 𝑥𝑦 𝑧𝑥 )
13 r19.29 ( ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ∧ ∃ 𝑥𝑦 𝑧𝑥 ) → ∃ 𝑥𝑦 ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) )
14 n0i ( 𝑧𝑥 → ¬ 𝑥 = ∅ )
15 14 adantl ( ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) → ¬ 𝑥 = ∅ )
16 simpl ( ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) → ( 𝑃𝑥𝑥 = ∅ ) )
17 16 ord ( ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) → ( ¬ 𝑃𝑥𝑥 = ∅ ) )
18 15 17 mt3d ( ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) → 𝑃𝑥 )
19 simpl ( ( 𝑥𝑦 ∧ ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) ) → 𝑥𝑦 )
20 elunii ( ( 𝑃𝑥𝑥𝑦 ) → 𝑃 𝑦 )
21 18 19 20 syl2an2 ( ( 𝑥𝑦 ∧ ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) ) → 𝑃 𝑦 )
22 21 rexlimiva ( ∃ 𝑥𝑦 ( ( 𝑃𝑥𝑥 = ∅ ) ∧ 𝑧𝑥 ) → 𝑃 𝑦 )
23 13 22 syl ( ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ∧ ∃ 𝑥𝑦 𝑧𝑥 ) → 𝑃 𝑦 )
24 23 ex ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) → ( ∃ 𝑥𝑦 𝑧𝑥𝑃 𝑦 ) )
25 24 ad2antll ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( ∃ 𝑥𝑦 𝑧𝑥𝑃 𝑦 ) )
26 12 25 syl5bi ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( 𝑧 𝑦𝑃 𝑦 ) )
27 26 exlimdv ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( ∃ 𝑧 𝑧 𝑦𝑃 𝑦 ) )
28 11 27 syl5bi ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( ¬ 𝑦 = ∅ → 𝑃 𝑦 ) )
29 28 con1d ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( ¬ 𝑃 𝑦 𝑦 = ∅ ) )
30 29 orrd ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → ( 𝑃 𝑦 𝑦 = ∅ ) )
31 4 10 30 elrabd ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
32 31 ex ( ( 𝐴𝑉𝑃𝐴 ) → ( ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = ∅ ) ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
33 1 32 syl5bi ( ( 𝐴𝑉𝑃𝐴 ) → ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
34 33 alrimiv ( ( 𝐴𝑉𝑃𝐴 ) → ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
35 eleq2 ( 𝑥 = 𝑦 → ( 𝑃𝑥𝑃𝑦 ) )
36 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = ∅ ↔ 𝑦 = ∅ ) )
37 35 36 orbi12d ( 𝑥 = 𝑦 → ( ( 𝑃𝑥𝑥 = ∅ ) ↔ ( 𝑃𝑦𝑦 = ∅ ) ) )
38 37 elrab ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) )
39 eleq2 ( 𝑥 = 𝑧 → ( 𝑃𝑥𝑃𝑧 ) )
40 eqeq1 ( 𝑥 = 𝑧 → ( 𝑥 = ∅ ↔ 𝑧 = ∅ ) )
41 39 40 orbi12d ( 𝑥 = 𝑧 → ( ( 𝑃𝑥𝑥 = ∅ ) ↔ ( 𝑃𝑧𝑧 = ∅ ) ) )
42 41 elrab ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) )
43 38 42 anbi12i ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) ↔ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) )
44 eleq2 ( 𝑥 = ( 𝑦𝑧 ) → ( 𝑃𝑥𝑃 ∈ ( 𝑦𝑧 ) ) )
45 eqeq1 ( 𝑥 = ( 𝑦𝑧 ) → ( 𝑥 = ∅ ↔ ( 𝑦𝑧 ) = ∅ ) )
46 44 45 orbi12d ( 𝑥 = ( 𝑦𝑧 ) → ( ( 𝑃𝑥𝑥 = ∅ ) ↔ ( 𝑃 ∈ ( 𝑦𝑧 ) ∨ ( 𝑦𝑧 ) = ∅ ) ) )
47 inss1 ( 𝑦𝑧 ) ⊆ 𝑦
48 simprll ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → 𝑦 ∈ 𝒫 𝐴 )
49 48 elpwid ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → 𝑦𝐴 )
50 47 49 sstrid ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑦𝑧 ) ⊆ 𝐴 )
51 vex 𝑦 ∈ V
52 51 inex1 ( 𝑦𝑧 ) ∈ V
53 52 elpw ( ( 𝑦𝑧 ) ∈ 𝒫 𝐴 ↔ ( 𝑦𝑧 ) ⊆ 𝐴 )
54 50 53 sylibr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑦𝑧 ) ∈ 𝒫 𝐴 )
55 ianor ( ¬ ( 𝑃𝑦𝑃𝑧 ) ↔ ( ¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧 ) )
56 elin ( 𝑃 ∈ ( 𝑦𝑧 ) ↔ ( 𝑃𝑦𝑃𝑧 ) )
57 55 56 xchnxbir ( ¬ 𝑃 ∈ ( 𝑦𝑧 ) ↔ ( ¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧 ) )
58 simprlr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑃𝑦𝑦 = ∅ ) )
59 58 ord ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( ¬ 𝑃𝑦𝑦 = ∅ ) )
60 simprrr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑃𝑧𝑧 = ∅ ) )
61 60 ord ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( ¬ 𝑃𝑧𝑧 = ∅ ) )
62 59 61 orim12d ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( ( ¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧 ) → ( 𝑦 = ∅ ∨ 𝑧 = ∅ ) ) )
63 57 62 syl5bi ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( ¬ 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦 = ∅ ∨ 𝑧 = ∅ ) ) )
64 inss ( ( 𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅ ) → ( 𝑦𝑧 ) ⊆ ∅ )
65 ss0b ( 𝑦 ⊆ ∅ ↔ 𝑦 = ∅ )
66 ss0b ( 𝑧 ⊆ ∅ ↔ 𝑧 = ∅ )
67 65 66 orbi12i ( ( 𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅ ) ↔ ( 𝑦 = ∅ ∨ 𝑧 = ∅ ) )
68 ss0b ( ( 𝑦𝑧 ) ⊆ ∅ ↔ ( 𝑦𝑧 ) = ∅ )
69 64 67 68 3imtr3i ( ( 𝑦 = ∅ ∨ 𝑧 = ∅ ) → ( 𝑦𝑧 ) = ∅ )
70 63 69 syl6 ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( ¬ 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = ∅ ) )
71 70 orrd ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑃 ∈ ( 𝑦𝑧 ) ∨ ( 𝑦𝑧 ) = ∅ ) )
72 46 54 71 elrabd ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) ) → ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
73 72 ex ( ( 𝐴𝑉𝑃𝐴 ) → ( ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = ∅ ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = ∅ ) ) ) → ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
74 43 73 syl5bi ( ( 𝐴𝑉𝑃𝐴 ) → ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) → ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
75 74 ralrimivv ( ( 𝐴𝑉𝑃𝐴 ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
76 pwexg ( 𝐴𝑉 → 𝒫 𝐴 ∈ V )
77 76 adantr ( ( 𝐴𝑉𝑃𝐴 ) → 𝒫 𝐴 ∈ V )
78 rabexg ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ V )
79 istopg ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ V → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) ) )
80 77 78 79 3syl ( ( 𝐴𝑉𝑃𝐴 ) → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) ) )
81 34 75 80 mpbir2and ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ Top )
82 eleq2 ( 𝑥 = 𝐴 → ( 𝑃𝑥𝑃𝐴 ) )
83 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = ∅ ↔ 𝐴 = ∅ ) )
84 82 83 orbi12d ( 𝑥 = 𝐴 → ( ( 𝑃𝑥𝑥 = ∅ ) ↔ ( 𝑃𝐴𝐴 = ∅ ) ) )
85 pwidg ( 𝐴𝑉𝐴 ∈ 𝒫 𝐴 )
86 85 adantr ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 ∈ 𝒫 𝐴 )
87 animorrl ( ( 𝐴𝑉𝑃𝐴 ) → ( 𝑃𝐴𝐴 = ∅ ) )
88 84 86 87 elrabd ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
89 elssuni ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } → 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
90 88 89 syl ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
91 ssrab2 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ⊆ 𝒫 𝐴
92 sspwuni ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ⊆ 𝒫 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ⊆ 𝐴 )
93 91 92 mpbi { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ⊆ 𝐴
94 93 a1i ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ⊆ 𝐴 )
95 90 94 eqssd ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } )
96 istopon ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) ↔ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ Top ∧ 𝐴 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ) )
97 81 95 96 sylanbrc ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = ∅ ) } ∈ ( TopOn ‘ 𝐴 ) )