| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > istopon | Structured version Visualization version GIF version | ||
| Description: Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.) |
| Ref | Expression |
|---|---|
| istopon | ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfvex 6944 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ V) | |
| 2 | uniexg 7760 | . . . 4 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V) | |
| 3 | eleq1 2829 | . . . 4 ⊢ (𝐵 = ∪ 𝐽 → (𝐵 ∈ V ↔ ∪ 𝐽 ∈ V)) | |
| 4 | 2, 3 | syl5ibrcom 247 | . . 3 ⊢ (𝐽 ∈ Top → (𝐵 = ∪ 𝐽 → 𝐵 ∈ V)) |
| 5 | 4 | imp 406 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽) → 𝐵 ∈ V) |
| 6 | eqeq1 2741 | . . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝑗)) | |
| 7 | 6 | rabbidv 3444 | . . . . 5 ⊢ (𝑏 = 𝐵 → {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗}) |
| 8 | df-topon 22917 | . . . . 5 ⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) | |
| 9 | vpwex 5377 | . . . . . . 7 ⊢ 𝒫 𝑏 ∈ V | |
| 10 | 9 | pwex 5380 | . . . . . 6 ⊢ 𝒫 𝒫 𝑏 ∈ V |
| 11 | rabss 4072 | . . . . . . 7 ⊢ ({𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏 ↔ ∀𝑗 ∈ Top (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏)) | |
| 12 | pwuni 4945 | . . . . . . . . . 10 ⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗 | |
| 13 | pweq 4614 | . . . . . . . . . 10 ⊢ (𝑏 = ∪ 𝑗 → 𝒫 𝑏 = 𝒫 ∪ 𝑗) | |
| 14 | 12, 13 | sseqtrrid 4027 | . . . . . . . . 9 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ⊆ 𝒫 𝑏) |
| 15 | velpw 4605 | . . . . . . . . 9 ⊢ (𝑗 ∈ 𝒫 𝒫 𝑏 ↔ 𝑗 ⊆ 𝒫 𝑏) | |
| 16 | 14, 15 | sylibr 234 | . . . . . . . 8 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏) |
| 17 | 16 | a1i 11 | . . . . . . 7 ⊢ (𝑗 ∈ Top → (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏)) |
| 18 | 11, 17 | mprgbir 3068 | . . . . . 6 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏 |
| 19 | 10, 18 | ssexi 5322 | . . . . 5 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ∈ V |
| 20 | 7, 8, 19 | fvmpt3i 7021 | . . . 4 ⊢ (𝐵 ∈ V → (TopOn‘𝐵) = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗}) |
| 21 | 20 | eleq2d 2827 | . . 3 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ 𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗})) |
| 22 | unieq 4918 | . . . . 5 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽) | |
| 23 | 22 | eqeq2d 2748 | . . . 4 ⊢ (𝑗 = 𝐽 → (𝐵 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝐽)) |
| 24 | 23 | elrab 3692 | . . 3 ⊢ (𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗} ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
| 25 | 21, 24 | bitrdi 287 | . 2 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))) |
| 26 | 1, 5, 25 | pm5.21nii 378 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {crab 3436 Vcvv 3480 ⊆ wss 3951 𝒫 cpw 4600 ∪ cuni 4907 ‘cfv 6561 Topctop 22899 TopOnctopon 22916 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-topon 22917 |
| This theorem is referenced by: topontop 22919 toponuni 22920 toptopon 22923 toponcom 22934 istps2 22941 tgtopon 22978 distopon 23004 indistopon 23008 fctop 23011 cctop 23013 ppttop 23014 epttop 23016 mretopd 23100 toponmre 23101 resttopon 23169 resttopon2 23176 kgentopon 23546 txtopon 23599 pttopon 23604 xkotopon 23608 qtoptopon 23712 flimtopon 23978 fclstopon 24020 fclsfnflim 24035 utoptopon 24245 qtopt1 33834 neibastop1 36360 onsuctopon 36435 rfcnpre1 45024 cnfex 45033 icccncfext 45902 stoweidlem47 46062 |
| Copyright terms: Public domain | W3C validator |