# Metamath Proof Explorer

## Theorem epttop

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

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

### Proof

Step Hyp Ref Expression
1 ssrab ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ↔ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) )
2 eleq2 ( 𝑥 = 𝑦 → ( 𝑃𝑥𝑃 𝑦 ) )
3 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 𝑦 = 𝐴 ) )
4 2 3 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑃𝑥𝑥 = 𝐴 ) ↔ ( 𝑃 𝑦 𝑦 = 𝐴 ) ) )
5 simprl ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → 𝑦 ⊆ 𝒫 𝐴 )
6 sspwuni ( 𝑦 ⊆ 𝒫 𝐴 𝑦𝐴 )
7 5 6 sylib ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → 𝑦𝐴 )
8 vuniex 𝑦 ∈ V
9 8 elpw ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴 )
10 7 9 sylibr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → 𝑦 ∈ 𝒫 𝐴 )
11 eluni2 ( 𝑃 𝑦 ↔ ∃ 𝑥𝑦 𝑃𝑥 )
12 r19.29 ( ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ∧ ∃ 𝑥𝑦 𝑃𝑥 ) → ∃ 𝑥𝑦 ( ( 𝑃𝑥𝑥 = 𝐴 ) ∧ 𝑃𝑥 ) )
13 simpr ( ( 𝑥𝑦 ∧ ( 𝑃𝑥𝑥 = 𝐴 ) ) → ( 𝑃𝑥𝑥 = 𝐴 ) )
14 13 impr ( ( 𝑥𝑦 ∧ ( ( 𝑃𝑥𝑥 = 𝐴 ) ∧ 𝑃𝑥 ) ) → 𝑥 = 𝐴 )
15 elssuni ( 𝑥𝑦𝑥 𝑦 )
16 15 adantr ( ( 𝑥𝑦 ∧ ( ( 𝑃𝑥𝑥 = 𝐴 ) ∧ 𝑃𝑥 ) ) → 𝑥 𝑦 )
17 14 16 eqsstrrd ( ( 𝑥𝑦 ∧ ( ( 𝑃𝑥𝑥 = 𝐴 ) ∧ 𝑃𝑥 ) ) → 𝐴 𝑦 )
18 17 rexlimiva ( ∃ 𝑥𝑦 ( ( 𝑃𝑥𝑥 = 𝐴 ) ∧ 𝑃𝑥 ) → 𝐴 𝑦 )
19 12 18 syl ( ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ∧ ∃ 𝑥𝑦 𝑃𝑥 ) → 𝐴 𝑦 )
20 19 ex ( ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) → ( ∃ 𝑥𝑦 𝑃𝑥𝐴 𝑦 ) )
21 20 ad2antll ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → ( ∃ 𝑥𝑦 𝑃𝑥𝐴 𝑦 ) )
22 11 21 syl5bi ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → ( 𝑃 𝑦𝐴 𝑦 ) )
23 22 7 jctild ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → ( 𝑃 𝑦 → ( 𝑦𝐴𝐴 𝑦 ) ) )
24 eqss ( 𝑦 = 𝐴 ↔ ( 𝑦𝐴𝐴 𝑦 ) )
25 23 24 syl6ibr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → ( 𝑃 𝑦 𝑦 = 𝐴 ) )
26 4 10 25 elrabd ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
27 26 ex ( ( 𝐴𝑉𝑃𝐴 ) → ( ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥𝑦 ( 𝑃𝑥𝑥 = 𝐴 ) ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) )
28 1 27 syl5bi ( ( 𝐴𝑉𝑃𝐴 ) → ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) )
29 28 alrimiv ( ( 𝐴𝑉𝑃𝐴 ) → ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) )
30 inss1 ( 𝑦𝑧 ) ⊆ 𝑦
31 simprll ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → 𝑦 ∈ 𝒫 𝐴 )
32 31 elpwid ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → 𝑦𝐴 )
33 30 32 sstrid ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( 𝑦𝑧 ) ⊆ 𝐴 )
34 vex 𝑦 ∈ V
35 34 inex1 ( 𝑦𝑧 ) ∈ V
36 35 elpw ( ( 𝑦𝑧 ) ∈ 𝒫 𝐴 ↔ ( 𝑦𝑧 ) ⊆ 𝐴 )
37 33 36 sylibr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( 𝑦𝑧 ) ∈ 𝒫 𝐴 )
38 elin ( 𝑃 ∈ ( 𝑦𝑧 ) ↔ ( 𝑃𝑦𝑃𝑧 ) )
39 simprlr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( 𝑃𝑦𝑦 = 𝐴 ) )
40 simprrr ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( 𝑃𝑧𝑧 = 𝐴 ) )
41 39 40 anim12d ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( ( 𝑃𝑦𝑃𝑧 ) → ( 𝑦 = 𝐴𝑧 = 𝐴 ) ) )
42 ineq12 ( ( 𝑦 = 𝐴𝑧 = 𝐴 ) → ( 𝑦𝑧 ) = ( 𝐴𝐴 ) )
43 inidm ( 𝐴𝐴 ) = 𝐴
44 42 43 eqtrdi ( ( 𝑦 = 𝐴𝑧 = 𝐴 ) → ( 𝑦𝑧 ) = 𝐴 )
45 41 44 syl6 ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( ( 𝑃𝑦𝑃𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) )
46 38 45 syl5bi ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) )
47 37 46 jca ( ( ( 𝐴𝑉𝑃𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) ) → ( ( 𝑦𝑧 ) ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) ) )
48 47 ex ( ( 𝐴𝑉𝑃𝐴 ) → ( ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) → ( ( 𝑦𝑧 ) ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) ) ) )
49 eleq2 ( 𝑥 = 𝑦 → ( 𝑃𝑥𝑃𝑦 ) )
50 eqeq1 ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴𝑦 = 𝐴 ) )
51 49 50 imbi12d ( 𝑥 = 𝑦 → ( ( 𝑃𝑥𝑥 = 𝐴 ) ↔ ( 𝑃𝑦𝑦 = 𝐴 ) ) )
52 51 elrab ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) )
53 eleq2 ( 𝑥 = 𝑧 → ( 𝑃𝑥𝑃𝑧 ) )
54 eqeq1 ( 𝑥 = 𝑧 → ( 𝑥 = 𝐴𝑧 = 𝐴 ) )
55 53 54 imbi12d ( 𝑥 = 𝑧 → ( ( 𝑃𝑥𝑥 = 𝐴 ) ↔ ( 𝑃𝑧𝑧 = 𝐴 ) ) )
56 55 elrab ( 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) )
57 52 56 anbi12i ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) ↔ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑦𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃𝑧𝑧 = 𝐴 ) ) ) )
58 eleq2 ( 𝑥 = ( 𝑦𝑧 ) → ( 𝑃𝑥𝑃 ∈ ( 𝑦𝑧 ) ) )
59 eqeq1 ( 𝑥 = ( 𝑦𝑧 ) → ( 𝑥 = 𝐴 ↔ ( 𝑦𝑧 ) = 𝐴 ) )
60 58 59 imbi12d ( 𝑥 = ( 𝑦𝑧 ) → ( ( 𝑃𝑥𝑥 = 𝐴 ) ↔ ( 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) ) )
61 60 elrab ( ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ↔ ( ( 𝑦𝑧 ) ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ ( 𝑦𝑧 ) → ( 𝑦𝑧 ) = 𝐴 ) ) )
62 48 57 61 3imtr4g ( ( 𝐴𝑉𝑃𝐴 ) → ( ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∧ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) → ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) )
63 62 ralrimivv ( ( 𝐴𝑉𝑃𝐴 ) → ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
64 pwexg ( 𝐴𝑉 → 𝒫 𝐴 ∈ V )
65 64 adantr ( ( 𝐴𝑉𝑃𝐴 ) → 𝒫 𝐴 ∈ V )
66 rabexg ( 𝒫 𝐴 ∈ V → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ V )
67 65 66 syl ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ V )
68 istopg ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ V → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) ) )
69 67 68 syl ( ( 𝐴𝑉𝑃𝐴 ) → ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ Top ↔ ( ∀ 𝑦 ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∀ 𝑧 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ( 𝑦𝑧 ) ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) ) )
70 29 63 69 mpbir2and ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ Top )
71 eleq2 ( 𝑥 = 𝐴 → ( 𝑃𝑥𝑃𝐴 ) )
72 eqeq1 ( 𝑥 = 𝐴 → ( 𝑥 = 𝐴𝐴 = 𝐴 ) )
73 71 72 imbi12d ( 𝑥 = 𝐴 → ( ( 𝑃𝑥𝑥 = 𝐴 ) ↔ ( 𝑃𝐴𝐴 = 𝐴 ) ) )
74 pwidg ( 𝐴𝑉𝐴 ∈ 𝒫 𝐴 )
75 74 adantr ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 ∈ 𝒫 𝐴 )
76 eqidd ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 = 𝐴 )
77 76 a1d ( ( 𝐴𝑉𝑃𝐴 ) → ( 𝑃𝐴𝐴 = 𝐴 ) )
78 73 75 77 elrabd ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
79 elssuni ( 𝐴 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } → 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
80 78 79 syl ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
81 ssrab2 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ⊆ 𝒫 𝐴
82 sspwuni ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ⊆ 𝒫 𝐴 { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ⊆ 𝐴 )
83 81 82 mpbi { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ⊆ 𝐴
84 83 a1i ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ⊆ 𝐴 )
85 80 84 eqssd ( ( 𝐴𝑉𝑃𝐴 ) → 𝐴 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } )
86 istopon ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ ( TopOn ‘ 𝐴 ) ↔ ( { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ Top ∧ 𝐴 = { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ) )
87 70 85 86 sylanbrc ( ( 𝐴𝑉𝑃𝐴 ) → { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃𝑥𝑥 = 𝐴 ) } ∈ ( TopOn ‘ 𝐴 ) )