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 ‘ 𝐴 ) )