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

Theorem ppttop 21543
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 4046 . . . . 5 (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅)))
2 eleq2 2898 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃 𝑦))
3 eqeq1 2822 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
42, 3orbi12d 912 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃 𝑦 𝑦 = ∅)))
5 simprl 767 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ⊆ 𝒫 𝐴)
6 sspwuni 5013 . . . . . . . . 9 (𝑦 ⊆ 𝒫 𝐴 𝑦𝐴)
75, 6sylib 219 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦𝐴)
8 vuniex 7455 . . . . . . . . 9 𝑦 ∈ V
98elpw 4542 . . . . . . . 8 ( 𝑦 ∈ 𝒫 𝐴 𝑦𝐴)
107, 9sylibr 235 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ∈ 𝒫 𝐴)
11 neq0 4306 . . . . . . . . . 10 𝑦 = ∅ ↔ ∃𝑧 𝑧 𝑦)
12 eluni2 4834 . . . . . . . . . . . 12 (𝑧 𝑦 ↔ ∃𝑥𝑦 𝑧𝑥)
13 r19.29 3251 . . . . . . . . . . . . . . 15 ((∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) ∧ ∃𝑥𝑦 𝑧𝑥) → ∃𝑥𝑦 ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥))
14 n0i 4296 . . . . . . . . . . . . . . . . . . 19 (𝑧𝑥 → ¬ 𝑥 = ∅)
1514adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → ¬ 𝑥 = ∅)
16 simpl 483 . . . . . . . . . . . . . . . . . . 19 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → (𝑃𝑥𝑥 = ∅))
1716ord 858 . . . . . . . . . . . . . . . . . 18 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → (¬ 𝑃𝑥𝑥 = ∅))
1815, 17mt3d 150 . . . . . . . . . . . . . . . . 17 (((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → 𝑃𝑥)
19 simpl 483 . . . . . . . . . . . . . . . . 17 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥)) → 𝑥𝑦)
20 elunii 4835 . . . . . . . . . . . . . . . . 17 ((𝑃𝑥𝑥𝑦) → 𝑃 𝑦)
2118, 19, 20syl2an2 682 . . . . . . . . . . . . . . . 16 ((𝑥𝑦 ∧ ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥)) → 𝑃 𝑦)
2221rexlimiva 3278 . . . . . . . . . . . . . . 15 (∃𝑥𝑦 ((𝑃𝑥𝑥 = ∅) ∧ 𝑧𝑥) → 𝑃 𝑦)
2313, 22syl 17 . . . . . . . . . . . . . 14 ((∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) ∧ ∃𝑥𝑦 𝑧𝑥) → 𝑃 𝑦)
2423ex 413 . . . . . . . . . . . . 13 (∀𝑥𝑦 (𝑃𝑥𝑥 = ∅) → (∃𝑥𝑦 𝑧𝑥𝑃 𝑦))
2524ad2antll 725 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (∃𝑥𝑦 𝑧𝑥𝑃 𝑦))
2612, 25syl5bi 243 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (𝑧 𝑦𝑃 𝑦))
2726exlimdv 1925 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (∃𝑧 𝑧 𝑦𝑃 𝑦))
2811, 27syl5bi 243 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (¬ 𝑦 = ∅ → 𝑃 𝑦))
2928con1d 147 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (¬ 𝑃 𝑦 𝑦 = ∅))
3029orrd 857 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → (𝑃 𝑦 𝑦 = ∅))
314, 10, 30elrabd 3679 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ (𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅))) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
3231ex 413 . . . . 5 ((𝐴𝑉𝑃𝐴) → ((𝑦 ⊆ 𝒫 𝐴 ∧ ∀𝑥𝑦 (𝑃𝑥𝑥 = ∅)) → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
331, 32syl5bi 243 . . . 4 ((𝐴𝑉𝑃𝐴) → (𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
3433alrimiv 1919 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
35 eleq2 2898 . . . . . . . 8 (𝑥 = 𝑦 → (𝑃𝑥𝑃𝑦))
36 eqeq1 2822 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥 = ∅ ↔ 𝑦 = ∅))
3735, 36orbi12d 912 . . . . . . 7 (𝑥 = 𝑦 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝑦𝑦 = ∅)))
3837elrab 3677 . . . . . 6 (𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)))
39 eleq2 2898 . . . . . . . 8 (𝑥 = 𝑧 → (𝑃𝑥𝑃𝑧))
40 eqeq1 2822 . . . . . . . 8 (𝑥 = 𝑧 → (𝑥 = ∅ ↔ 𝑧 = ∅))
4139, 40orbi12d 912 . . . . . . 7 (𝑥 = 𝑧 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝑧𝑧 = ∅)))
4241elrab 3677 . . . . . 6 (𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ↔ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))
4338, 42anbi12i 626 . . . . 5 ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ↔ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅))))
44 eleq2 2898 . . . . . . . 8 (𝑥 = (𝑦𝑧) → (𝑃𝑥𝑃 ∈ (𝑦𝑧)))
45 eqeq1 2822 . . . . . . . 8 (𝑥 = (𝑦𝑧) → (𝑥 = ∅ ↔ (𝑦𝑧) = ∅))
4644, 45orbi12d 912 . . . . . . 7 (𝑥 = (𝑦𝑧) → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃 ∈ (𝑦𝑧) ∨ (𝑦𝑧) = ∅)))
47 inss1 4202 . . . . . . . . 9 (𝑦𝑧) ⊆ 𝑦
48 simprll 775 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → 𝑦 ∈ 𝒫 𝐴)
4948elpwid 4549 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → 𝑦𝐴)
5047, 49sstrid 3975 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ⊆ 𝐴)
51 vex 3495 . . . . . . . . . 10 𝑦 ∈ V
5251inex1 5212 . . . . . . . . 9 (𝑦𝑧) ∈ V
5352elpw 4542 . . . . . . . 8 ((𝑦𝑧) ∈ 𝒫 𝐴 ↔ (𝑦𝑧) ⊆ 𝐴)
5450, 53sylibr 235 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ∈ 𝒫 𝐴)
55 ianor 975 . . . . . . . . . . 11 (¬ (𝑃𝑦𝑃𝑧) ↔ (¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧))
56 elin 4166 . . . . . . . . . . 11 (𝑃 ∈ (𝑦𝑧) ↔ (𝑃𝑦𝑃𝑧))
5755, 56xchnxbir 334 . . . . . . . . . 10 𝑃 ∈ (𝑦𝑧) ↔ (¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧))
58 simprlr 776 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃𝑦𝑦 = ∅))
5958ord 858 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃𝑦𝑦 = ∅))
60 simprrr 778 . . . . . . . . . . . 12 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃𝑧𝑧 = ∅))
6160ord 858 . . . . . . . . . . 11 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃𝑧𝑧 = ∅))
6259, 61orim12d 958 . . . . . . . . . 10 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → ((¬ 𝑃𝑦 ∨ ¬ 𝑃𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅)))
6357, 62syl5bi 243 . . . . . . . . 9 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦𝑧) → (𝑦 = ∅ ∨ 𝑧 = ∅)))
64 inss 4212 . . . . . . . . . 10 ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) → (𝑦𝑧) ⊆ ∅)
65 ss0b 4348 . . . . . . . . . . 11 (𝑦 ⊆ ∅ ↔ 𝑦 = ∅)
66 ss0b 4348 . . . . . . . . . . 11 (𝑧 ⊆ ∅ ↔ 𝑧 = ∅)
6765, 66orbi12i 908 . . . . . . . . . 10 ((𝑦 ⊆ ∅ ∨ 𝑧 ⊆ ∅) ↔ (𝑦 = ∅ ∨ 𝑧 = ∅))
68 ss0b 4348 . . . . . . . . . 10 ((𝑦𝑧) ⊆ ∅ ↔ (𝑦𝑧) = ∅)
6964, 67, 683imtr3i 292 . . . . . . . . 9 ((𝑦 = ∅ ∨ 𝑧 = ∅) → (𝑦𝑧) = ∅)
7063, 69syl6 35 . . . . . . . 8 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (¬ 𝑃 ∈ (𝑦𝑧) → (𝑦𝑧) = ∅))
7170orrd 857 . . . . . . 7 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑃 ∈ (𝑦𝑧) ∨ (𝑦𝑧) = ∅))
7246, 54, 71elrabd 3679 . . . . . 6 (((𝐴𝑉𝑃𝐴) ∧ ((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅)))) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
7372ex 413 . . . . 5 ((𝐴𝑉𝑃𝐴) → (((𝑦 ∈ 𝒫 𝐴 ∧ (𝑃𝑦𝑦 = ∅)) ∧ (𝑧 ∈ 𝒫 𝐴 ∧ (𝑃𝑧𝑧 = ∅))) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
7443, 73syl5bi 243 . . . 4 ((𝐴𝑉𝑃𝐴) → ((𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∧ 𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) → (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
7574ralrimivv 3187 . . 3 ((𝐴𝑉𝑃𝐴) → ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
76 pwexg 5270 . . . . 5 (𝐴𝑉 → 𝒫 𝐴 ∈ V)
7776adantr 481 . . . 4 ((𝐴𝑉𝑃𝐴) → 𝒫 𝐴 ∈ V)
78 rabexg 5225 . . . 4 (𝒫 𝐴 ∈ V → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ V)
79 istopg 21431 . . . 4 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ V → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})))
8077, 78, 793syl 18 . . 3 ((𝐴𝑉𝑃𝐴) → ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ↔ (∀𝑦(𝑦 ⊆ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}) ∧ ∀𝑦 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}∀𝑧 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} (𝑦𝑧) ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})))
8134, 75, 80mpbir2and 709 . 2 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top)
82 eleq2 2898 . . . . . 6 (𝑥 = 𝐴 → (𝑃𝑥𝑃𝐴))
83 eqeq1 2822 . . . . . 6 (𝑥 = 𝐴 → (𝑥 = ∅ ↔ 𝐴 = ∅))
8482, 83orbi12d 912 . . . . 5 (𝑥 = 𝐴 → ((𝑃𝑥𝑥 = ∅) ↔ (𝑃𝐴𝐴 = ∅)))
85 pwidg 4552 . . . . . 6 (𝐴𝑉𝐴 ∈ 𝒫 𝐴)
8685adantr 481 . . . . 5 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ 𝒫 𝐴)
87 animorrl 974 . . . . 5 ((𝐴𝑉𝑃𝐴) → (𝑃𝐴𝐴 = ∅))
8884, 86, 87elrabd 3679 . . . 4 ((𝐴𝑉𝑃𝐴) → 𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
89 elssuni 4859 . . . 4 (𝐴 ∈ {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
9088, 89syl 17 . . 3 ((𝐴𝑉𝑃𝐴) → 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
91 ssrab2 4053 . . . . 5 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝒫 𝐴
92 sspwuni 5013 . . . . 5 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝒫 𝐴 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴)
9391, 92mpbi 231 . . . 4 {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴
9493a1i 11 . . 3 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ⊆ 𝐴)
9590, 94eqssd 3981 . 2 ((𝐴𝑉𝑃𝐴) → 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)})
96 istopon 21448 . 2 ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ (TopOn‘𝐴) ↔ ({𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ Top ∧ 𝐴 = {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)}))
9781, 95, 96sylanbrc 583 1 ((𝐴𝑉𝑃𝐴) → {𝑥 ∈ 𝒫 𝐴 ∣ (𝑃𝑥𝑥 = ∅)} ∈ (TopOn‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  wal 1526   = wceq 1528  wex 1771  wcel 2105  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cin 3932  wss 3933  c0 4288  𝒫 cpw 4535   cuni 4830  cfv 6348  Topctop 21429  TopOnctopon 21446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fv 6356  df-top 21430  df-topon 21447
This theorem is referenced by:  pptbas  21544
  Copyright terms: Public domain W3C validator