![]() |
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 21517 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) | |
3 | 1, 2 | mpbiran2 709 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top) |
4 | 3 | bicomi 227 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1538 ∈ wcel 2111 ∪ cuni 4800 ‘cfv 6324 Topctop 21498 TopOnctopon 21515 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 df-topon 21516 |
This theorem is referenced by: toptopon2 21523 eltpsi 21549 restuni 21767 stoig 21768 restlp 21788 restperf 21789 perfopn 21790 iscn2 21843 iscnp2 21844 cncnpi 21883 cncnp2 21886 cnnei 21887 cnrest 21890 cnpresti 21893 cnprest 21894 cnprest2 21895 paste 21899 t1sep2 21974 sshauslem 21977 1stcelcls 22066 kgenuni 22144 iskgen3 22154 txuni 22197 ptuniconst 22203 txcnmpt 22229 txcn 22231 txindis 22239 ptrescn 22244 txcmpb 22249 xkoptsub 22259 xkofvcn 22289 imasnopn 22295 imasncld 22296 imasncls 22297 qtopcmplem 22312 qtopkgen 22315 hmeof1o 22369 hmeores 22376 hmphindis 22402 cmphaushmeo 22405 txhmeo 22408 ptunhmeo 22413 hausflim 22586 flfneii 22597 hausflf 22602 flimfnfcls 22633 flfcntr 22648 cnextfun 22669 cnextfvval 22670 cnextf 22671 cnextcn 22672 cnextfres1 22673 retopon 23369 evth 23564 evth2 23565 qtophaus 31189 rrhre 31372 pconnconn 32591 connpconn 32595 pconnpi1 32597 sconnpi1 32599 txsconnlem 32600 txsconn 32601 cvxsconn 32603 cvmsf1o 32632 cvmliftmolem1 32641 cvmliftlem8 32652 cvmlift2lem9a 32663 cvmlift2lem9 32671 cvmlift2lem11 32673 cvmlift2lem12 32674 cvmliftphtlem 32677 cvmlift3lem6 32684 cvmlift3lem8 32686 cvmlift3lem9 32687 cnres2 35201 cnresima 35202 hausgraph 40156 ntrf2 40827 fcnre 41654 |
Copyright terms: Public domain | W3C validator |