Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > toptopon2 | Structured version Visualization version GIF version |
Description: A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) |
Ref | Expression |
---|---|
toptopon2 | ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2823 | . 2 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | toptopon 21527 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∈ wcel 2114 ∪ cuni 4840 ‘cfv 6357 Topctop 21503 TopOnctopon 21520 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-iota 6316 df-fun 6359 df-fv 6365 df-topon 21521 |
This theorem is referenced by: topontopon 21529 toprntopon 21535 neiptopreu 21743 lmcvg 21872 cnss1 21886 cnss2 21887 cnrest2 21896 cnrest2r 21897 lmss 21908 lmcnp 21914 lmcn 21915 t1t0 21958 haust1 21962 restcnrm 21972 resthauslem 21973 lmmo 21990 rncmp 22006 connima 22035 conncn 22036 kgeni 22147 kgenftop 22150 kgenss 22153 kgenhaus 22154 kgencmp2 22156 kgenidm 22157 1stckgen 22164 kgencn3 22168 kgen2cn 22169 dfac14 22228 ptcnplem 22231 ptcnp 22232 txcnmpt 22234 ptcn 22237 txdis1cn 22245 lmcn2 22259 txkgen 22262 xkohaus 22263 xkopt 22265 cnmpt11 22273 cnmpt11f 22274 cnmpt1t 22275 cnmpt12 22277 cnmpt21 22281 cnmpt21f 22282 cnmpt2t 22283 cnmpt22 22284 cnmpt22f 22285 cnmptcom 22288 cnmptkp 22290 cnmpt2k 22298 txconn 22299 qtopss 22325 qtopeu 22326 qtopomap 22328 qtopcmap 22329 kqtop 22355 kqt0 22356 nrmr0reg 22359 regr1 22360 kqreg 22361 kqnrm 22362 hmeoqtop 22385 hmphref 22391 xpstopnlem1 22419 ptcmpfi 22423 xkocnv 22424 xkohmeo 22425 kqhmph 22429 flimsncls 22596 cnpflfi 22609 flfcnp 22614 flfcnp2 22617 cnpfcfi 22650 cnextucn 22914 cnmpopc 23534 htpyco1 23584 htpyco2 23585 phtpyco2 23596 pcopt 23628 pcopt2 23629 pcorevlem 23632 pi1cof 23665 pi1coghm 23667 |
Copyright terms: Public domain | W3C validator |