![]() |
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 6466 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ V) | |
2 | uniexg 7214 | . . . 4 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ V) | |
3 | eleq1 2893 | . . . 4 ⊢ (𝐵 = ∪ 𝐽 → (𝐵 ∈ V ↔ ∪ 𝐽 ∈ V)) | |
4 | 2, 3 | syl5ibrcom 239 | . . 3 ⊢ (𝐽 ∈ Top → (𝐵 = ∪ 𝐽 → 𝐵 ∈ V)) |
5 | 4 | imp 397 | . 2 ⊢ ((𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽) → 𝐵 ∈ V) |
6 | eqeq1 2828 | . . . . . 6 ⊢ (𝑏 = 𝐵 → (𝑏 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝑗)) | |
7 | 6 | rabbidv 3401 | . . . . 5 ⊢ (𝑏 = 𝐵 → {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗}) |
8 | df-topon 21085 | . . . . 5 ⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) | |
9 | vpwex 5076 | . . . . . . 7 ⊢ 𝒫 𝑏 ∈ V | |
10 | 9 | pwex 5079 | . . . . . 6 ⊢ 𝒫 𝒫 𝑏 ∈ V |
11 | rabss 3903 | . . . . . . 7 ⊢ ({𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏 ↔ ∀𝑗 ∈ Top (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏)) | |
12 | pwuni 4695 | . . . . . . . . . 10 ⊢ 𝑗 ⊆ 𝒫 ∪ 𝑗 | |
13 | pweq 4380 | . . . . . . . . . 10 ⊢ (𝑏 = ∪ 𝑗 → 𝒫 𝑏 = 𝒫 ∪ 𝑗) | |
14 | 12, 13 | syl5sseqr 3878 | . . . . . . . . 9 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ⊆ 𝒫 𝑏) |
15 | selpw 4384 | . . . . . . . . 9 ⊢ (𝑗 ∈ 𝒫 𝒫 𝑏 ↔ 𝑗 ⊆ 𝒫 𝑏) | |
16 | 14, 15 | sylibr 226 | . . . . . . . 8 ⊢ (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏) |
17 | 16 | a1i 11 | . . . . . . 7 ⊢ (𝑗 ∈ Top → (𝑏 = ∪ 𝑗 → 𝑗 ∈ 𝒫 𝒫 𝑏)) |
18 | 11, 17 | mprgbir 3135 | . . . . . 6 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ⊆ 𝒫 𝒫 𝑏 |
19 | 10, 18 | ssexi 5027 | . . . . 5 ⊢ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗} ∈ V |
20 | 7, 8, 19 | fvmpt3i 6533 | . . . 4 ⊢ (𝐵 ∈ V → (TopOn‘𝐵) = {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗}) |
21 | 20 | eleq2d 2891 | . . 3 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ 𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗})) |
22 | unieq 4665 | . . . . 5 ⊢ (𝑗 = 𝐽 → ∪ 𝑗 = ∪ 𝐽) | |
23 | 22 | eqeq2d 2834 | . . . 4 ⊢ (𝑗 = 𝐽 → (𝐵 = ∪ 𝑗 ↔ 𝐵 = ∪ 𝐽)) |
24 | 23 | elrab 3584 | . . 3 ⊢ (𝐽 ∈ {𝑗 ∈ Top ∣ 𝐵 = ∪ 𝑗} ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
25 | 21, 24 | syl6bb 279 | . 2 ⊢ (𝐵 ∈ V → (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))) |
26 | 1, 5, 25 | pm5.21nii 370 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1658 ∈ wcel 2166 {crab 3120 Vcvv 3413 ⊆ wss 3797 𝒫 cpw 4377 ∪ cuni 4657 ‘cfv 6122 Topctop 21067 TopOnctopon 21084 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 ax-un 7208 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-pw 4379 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-iota 6085 df-fun 6124 df-fv 6130 df-topon 21085 |
This theorem is referenced by: topontop 21087 toponuni 21088 toptopon 21091 toponcom 21102 istps2 21109 tgtopon 21145 distopon 21171 indistopon 21175 fctop 21178 cctop 21180 ppttop 21181 epttop 21183 mretopd 21266 toponmre 21267 resttopon 21335 resttopon2 21342 kgentopon 21711 txtopon 21764 pttopon 21769 xkotopon 21773 qtoptopon 21877 flimtopon 22143 fclstopon 22185 fclsfnflim 22200 utoptopon 22409 qtopt1 30446 neibastop1 32891 onsuctopon 32965 rfcnpre1 39995 cnfex 40004 icccncfext 40894 stoweidlem47 41057 |
Copyright terms: Public domain | W3C validator |