Metamath Proof Explorer

Theorem ppttop

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

Ref Expression
Assertion ppttop ⊢ A ∈ V ∧ P ∈ A → x ∈ 𝒫 A | P ∈ x ∨ x = ∅ ∈ TopOn ⁡ A

Proof

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