![]() |
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 2779 | . 2 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
2 | 1 | toptopon 21229 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∈ wcel 2050 ∪ cuni 4712 ‘cfv 6188 Topctop 21205 TopOnctopon 21222 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2751 ax-sep 5060 ax-nul 5067 ax-pow 5119 ax-pr 5186 ax-un 7279 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2760 df-cleq 2772 df-clel 2847 df-nfc 2919 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3418 df-sbc 3683 df-dif 3833 df-un 3835 df-in 3837 df-ss 3844 df-nul 4180 df-if 4351 df-pw 4424 df-sn 4442 df-pr 4444 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-mpt 5009 df-id 5312 df-xp 5413 df-rel 5414 df-cnv 5415 df-co 5416 df-dm 5417 df-iota 6152 df-fun 6190 df-fv 6196 df-topon 21223 |
This theorem is referenced by: topontopon 21231 toprntopon 21237 neiptopreu 21445 lmcvg 21574 cnss1 21588 cnss2 21589 cnrest2 21598 cnrest2r 21599 lmss 21610 lmcnp 21616 lmcn 21617 t1t0 21660 haust1 21664 restcnrm 21674 resthauslem 21675 lmmo 21692 rncmp 21708 connima 21737 conncn 21738 kgeni 21849 kgenftop 21852 kgenss 21855 kgenhaus 21856 kgencmp2 21858 kgenidm 21859 1stckgen 21866 kgencn3 21870 kgen2cn 21871 dfac14 21930 ptcnplem 21933 ptcnp 21934 txcnmpt 21936 ptcn 21939 txdis1cn 21947 lmcn2 21961 txkgen 21964 xkohaus 21965 xkopt 21967 cnmpt11 21975 cnmpt11f 21976 cnmpt1t 21977 cnmpt12 21979 cnmpt21 21983 cnmpt21f 21984 cnmpt2t 21985 cnmpt22 21986 cnmpt22f 21987 cnmptcom 21990 cnmptkp 21992 cnmpt2k 22000 txconn 22001 qtopss 22027 qtopeu 22028 qtopomap 22030 qtopcmap 22031 kqtop 22057 kqt0 22058 nrmr0reg 22061 regr1 22062 kqreg 22063 kqnrm 22064 hmeoqtop 22087 hmphref 22093 xpstopnlem1 22121 ptcmpfi 22125 xkocnv 22126 xkohmeo 22127 kqhmph 22131 flimsncls 22298 cnpflfi 22311 flfcnp 22316 flfcnp2 22319 cnpfcfi 22352 cnextucn 22615 cnmpopc 23235 htpyco1 23285 htpyco2 23286 phtpyco2 23297 pcopt 23329 pcopt2 23330 pcorevlem 23333 pi1cof 23366 pi1coghm 23368 |
Copyright terms: Public domain | W3C validator |