Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ppttop Structured version   Visualization version   GIF version

Theorem ppttop 21707
 Description: The particular point topology. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
ppttop ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ (TopOn‘𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝑃   𝑥,𝑉

Proof of Theorem ppttop
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab 3977 . . . . 5 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅)))
2 eleq2 2840 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃 𝑦))
3 eqeq1 2762 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
42, 3orbi12d 916 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃 𝑦 𝑦 = ∅)))
5 simprl 770 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ⊆ 𝒫 𝐴)
6 sspwuni 4987 . . . . . . . . 9 (𝑦 ⊆ 𝒫 𝐴 𝑦𝐴)
75, 6sylib 221 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦𝐴)
8 vuniex 7463 . . . . . . . . 9 𝑦 ∈ V
98elpw 4498 . . . . . . . 8 ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴)
107, 9sylibr 237 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ∈ 𝒫 𝐴)
11 neq0 4244 . . . . . . . . . 10 𝑦 = ∅ ↔ ∃𝑧 𝑧 𝑦)
12 eluni2 4802 . . . . . . . . . . . 12 (𝑧 𝑦 ↔ ∃𝑥𝑦 𝑧𝑥)
13 r19.29 3181 . . . . . . . . . . . . . . 15 ((∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) ∧ ∃𝑥𝑦 𝑧𝑥) → ∃𝑥𝑦 ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥))
14 n0i 4232 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ¬ 𝑥 = ∅)
1514adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → ¬ 𝑥 = ∅)
16 simpl 486 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → (𝑃𝑥𝑥 = ∅))
1716ord 861 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → (¬ 𝑃𝑥𝑥 = ∅))
1815, 17mt3d 150 . . . . . . . . . . . . . . . . 17 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → 𝑃𝑥)
19 simpl 486 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥)) → 𝑥𝑦)
20 elunii 4803 . . . . . . . . . . . . . . . . 17 ((𝑃𝑥𝑥𝑦) → 𝑃 𝑦)
2118, 19, 20syl2an2 685 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥)) → 𝑃 𝑦)
2221rexlimiva 3205 . . . . . . . . . . . . . . 15 (∃𝑥𝑦 ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → 𝑃 𝑦)
2313, 22syl 17 . . . . . . . . . . . . . 14 ((∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) ∧ ∃𝑥𝑦 𝑧𝑥) → 𝑃 𝑦)
2423ex 416 . . . . . . . . . . . . 13 (∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) → (∃𝑥𝑦 𝑧𝑥𝑃 𝑦))
2524ad2antll 728 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (∃𝑥𝑦 𝑧𝑥𝑃 𝑦))
2612, 25syl5bi 245 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (𝑧 𝑦𝑃 𝑦))
2726exlimdv 1934 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (∃𝑧 𝑧 𝑦𝑃 𝑦))
2811, 27syl5bi 245 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (¬ 𝑦 = ∅ → 𝑃 𝑦))
2928con1d 147 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (¬ 𝑃 𝑦 𝑦 = ∅))
3029orrd 860 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (𝑃 𝑦 𝑦 = ∅))
314, 10, 30elrabd 3604 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
3231ex 416 . . . . 5 ((𝐴𝑉𝑃𝐴) → ((𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅)) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
331, 32syl5bi 245 . . . 4 ((𝐴𝑉𝑃𝐴) → (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
3433alrimiv 1928 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
35 eleq2 2840 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃𝑦))
36 eqeq1 2762 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
3735, 36orbi12d 916 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝑦𝑦 = ∅)))
3837elrab 3602 . . . . . 6 (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)))
39 eleq2 2840 . . . . . . . 8 (𝑥 = 𝑧 → (𝑃𝑥𝑃𝑧))
40 eqeq1 2762 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅))
4139, 40orbi12d 916 . . . . . . 7 (𝑥 = 𝑧 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝑧𝑧 = ∅)))
4241elrab 3602 . . . . . 6 (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))
4338, 42anbi12i 629 . . . . 5 ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅))))
44 eleq2 2840 . . . . . . . 8 (𝑥 = (𝑦𝑧) → (𝑃𝑥𝑃 ∈ (𝑦𝑧)))
45 eqeq1 2762 . . . . . . . 8 (𝑥 = (𝑦𝑧) → (𝑥 = ∅ ↔ (𝑦𝑧) = ∅))
4644, 45orbi12d 916 . . . . . . 7 (𝑥 = (𝑦𝑧) → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃 ∈ (𝑦𝑧) ∨ (𝑦𝑧) = ∅)))
47 inss1 4133 . . . . . . . . 9 (𝑦𝑧) ⊆ 𝑦
48 simprll 778 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → 𝑦 ∈ 𝒫 𝐴)
4948elpwid 4505 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → 𝑦𝐴)
5047, 49sstrid 3903 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ⊆ 𝐴)
51 vex 3413 . . . . . . . . . 10 𝑦 ∈ V
5251inex1 5187 . . . . . . . . 9 (𝑦𝑧) ∈ V
5352elpw 4498 . . . . . . . 8 ((𝑦𝑧) ∈ 𝒫 𝐴 ↔ (𝑦𝑧) ⊆ 𝐴)
5450, 53sylibr 237 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ∈ 𝒫 𝐴)
55 ianor 979 . . . . . . . . . . 11 (¬ (𝑃𝑦𝑃𝑧) ↔ (¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧))
56 elin 3874 . . . . . . . . . . 11 (𝑃 ∈ (𝑦𝑧) ↔ (𝑃𝑦𝑃𝑧))
5755, 56xchnxbir 336 . . . . . . . . . 10 𝑃 ∈ (𝑦𝑧) ↔ (¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧))
58 simprlr 779 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃𝑦𝑦 = ∅))
5958ord 861 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃𝑦𝑦 = ∅))
60 simprrr 781 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃𝑧𝑧 = ∅))
6160ord 861 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃𝑧𝑧 = ∅))
6259, 61orim12d 962 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → ((¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅)))
6357, 62syl5bi 245 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅)))
64 inss 4143 . . . . . . . . . 10 ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) → (𝑦𝑧) ⊆ ∅)
65 ss0b 4293 . . . . . . . . . . 11 (𝑦 ⊆ ∅ ↔ 𝑦 = ∅)
66 ss0b 4293 . . . . . . . . . . 11 (𝑧 ⊆ ∅ ↔ 𝑧 = ∅)
6765, 66orbi12i 912 . . . . . . . . . 10 ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) ↔ (𝑦 = ∅ ∨ 𝑧 = ∅))
68 ss0b 4293 . . . . . . . . . 10 ((𝑦𝑧) ⊆ ∅ ↔ (𝑦𝑧) = ∅)
6964, 67, 683imtr3i 294 . . . . . . . . 9 ((𝑦 = ∅ ∨ 𝑧 = ∅) → (𝑦𝑧) = ∅)
7063, 69syl6 35 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = ∅))
7170orrd 860 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃 ∈ (𝑦𝑧) ∨ (𝑦𝑧) = ∅))
7246, 54, 71elrabd 3604 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
7372ex 416 . . . . 5 ((𝐴𝑉𝑃𝐴) → (((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅))) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
7443, 73syl5bi 245 . . . 4 ((𝐴𝑉𝑃𝐴) → ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
7574ralrimivv 3119 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
76 pwexg 5247 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
7776adantr 484 . . . 4 ((𝐴𝑉𝑃𝐴) → 𝒫 𝐴 ∈ V)
78 rabexg 5201 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ V)
79 istopg 21595 . . . 4 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})))
8077, 78, 793syl 18 . . 3 ((𝐴𝑉𝑃𝐴) → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})))
8134, 75, 80mpbir2and 712 . 2 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top)
82 eleq2 2840 . . . . . 6 (𝑥 = 𝐴 → (𝑃𝑥𝑃𝐴))
83 eqeq1 2762 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅))
8482, 83orbi12d 916 . . . . 5 (𝑥 = 𝐴 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝐴𝐴 = ∅)))
85 pwidg 4516 . . . . . 6 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
8685adantr 484 . . . . 5 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ 𝒫 𝐴)
87 animorrl 978 . . . . 5 ((𝐴𝑉𝑃𝐴) → (𝑃𝐴𝐴 = ∅))
8884, 86, 87elrabd 3604 . . . 4 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
89 elssuni 4830 . . . 4 (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
9088, 89syl 17 . . 3 ((𝐴𝑉𝑃𝐴) → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
91 ssrab2 3984 . . . . 5 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝒫 𝐴
92 sspwuni 4987 . . . . 5 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝒫 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴)
9391, 92mpbi 233 . . . 4 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴
9493a1i 11 . . 3 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴)
9590, 94eqssd 3909 . 2 ((𝐴𝑉𝑃𝐴) → 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
96 istopon 21612 . 2 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ∧ 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
9781, 95, 96sylanbrc 586 1 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ (TopOn‘𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  {crab 3074  Vcvv 3409   ∩ cin 3857   ⊆ wss 3858  ∅c0 4225  𝒫 cpw 4494  ∪ cuni 4798  ‘cfv 6335  Topctop 21593  TopOnctopon 21610 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-iota 6294  df-fun 6337  df-fv 6343  df-top 21594  df-topon 21611 This theorem is referenced by:  pptbas  21708
 Copyright terms: Public domain W3C validator