Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > toptopon | Structured version Visualization version GIF version |
Description: Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toptopon.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
toptopon | ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toptopon.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
2 | istopon 21841 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) | |
3 | 1, 2 | mpbiran2 710 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top) |
4 | 3 | bicomi 227 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ∈ wcel 2112 ∪ cuni 4836 ‘cfv 6401 Topctop 21822 TopOnctopon 21839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3425 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5153 df-id 5472 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-iota 6359 df-fun 6403 df-fv 6409 df-topon 21840 |
This theorem is referenced by: toptopon2 21847 eltpsi 21873 restuni 22091 stoig 22092 restlp 22112 restperf 22113 perfopn 22114 iscn2 22167 iscnp2 22168 cncnpi 22207 cncnp2 22210 cnnei 22211 cnrest 22214 cnpresti 22217 cnprest 22218 cnprest2 22219 paste 22223 t1sep2 22298 sshauslem 22301 1stcelcls 22390 kgenuni 22468 iskgen3 22478 txuni 22521 ptuniconst 22527 txcnmpt 22553 txcn 22555 txindis 22563 ptrescn 22568 txcmpb 22573 xkoptsub 22583 xkofvcn 22613 imasnopn 22619 imasncld 22620 imasncls 22621 qtopcmplem 22636 qtopkgen 22639 hmeof1o 22693 hmeores 22700 hmphindis 22726 cmphaushmeo 22729 txhmeo 22732 ptunhmeo 22737 hausflim 22910 flfneii 22921 hausflf 22926 flimfnfcls 22957 flfcntr 22972 cnextfun 22993 cnextfvval 22994 cnextf 22995 cnextcn 22996 cnextfres1 22997 retopon 23693 evth 23888 evth2 23889 qtophaus 31532 rrhre 31715 pconnconn 32937 connpconn 32941 pconnpi1 32943 sconnpi1 32945 txsconnlem 32946 txsconn 32947 cvxsconn 32949 cvmsf1o 32978 cvmliftmolem1 32987 cvmliftlem8 32998 cvmlift2lem9a 33009 cvmlift2lem9 33017 cvmlift2lem11 33019 cvmlift2lem12 33020 cvmliftphtlem 33023 cvmlift3lem6 33030 cvmlift3lem8 33032 cvmlift3lem9 33033 cnres2 35695 cnresima 35696 hausgraph 40788 ntrf2 41459 fcnre 42289 |
Copyright terms: Public domain | W3C validator |