This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) ) ) → ( 𝑃 ∈ ∪ 𝑦 → 𝐴 ⊆ ∪ 𝑦 ) )
23 22 7 jctild ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) ) ) → ( 𝑃 ∈ ∪ 𝑦 → ( ∪ 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) )
24 eqss ⊢ ( ∪ 𝑦 = 𝐴 ↔ ( ∪ 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) )
25 23 24 imbitrrdi ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) ) ) → ( 𝑃 ∈ ∪ 𝑦 → ∪ 𝑦 = 𝐴 ) )
26 4 10 25 elrabd ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) ) ) → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) } )
27 26 ex ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( ( 𝑦 ⊆ 𝒫 𝐴 ∧ ∀ 𝑥 ∈ 𝑦 ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) ) → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) } ) )
28 1 27 biimtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) → ( 𝑦 ⊆ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) } → ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ( 𝑃 ∈ 𝑥 → 𝑥 = 𝐴 ) } ) )
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 biimtrid ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴 ) ∧ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑦 → 𝑦 = 𝐴 ) ) ∧ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑃 ∈ 𝑧 → 𝑧 = 𝐴 ) ) ) ) → ( 𝑃 ∈ ( 𝑦 ∩ 𝑧 ) → ( 𝑦 ∩ 𝑧 ) = 𝐴 ) )
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 ‘ 𝐴 ) )