![]() |
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 22834 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) | |
3 | 1, 2 | mpbiran2 708 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top) |
4 | 3 | bicomi 223 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ∈ wcel 2098 ∪ cuni 4912 ‘cfv 6553 Topctop 22815 TopOnctopon 22832 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-sep 5303 ax-nul 5310 ax-pow 5369 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ral 3059 df-rex 3068 df-rab 3431 df-v 3475 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-br 5153 df-opab 5215 df-mpt 5236 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-iota 6505 df-fun 6555 df-fv 6561 df-topon 22833 |
This theorem is referenced by: toptopon2 22840 eltpsi 22867 restuni 23086 stoig 23087 restlp 23107 restperf 23108 perfopn 23109 iscn2 23162 iscnp2 23163 cncnpi 23202 cncnp2 23205 cnnei 23206 cnrest 23209 cnpresti 23212 cnprest 23213 cnprest2 23214 paste 23218 t1sep2 23293 sshauslem 23296 1stcelcls 23385 kgenuni 23463 iskgen3 23473 txuni 23516 ptuniconst 23522 txcnmpt 23548 txcn 23550 txindis 23558 ptrescn 23563 txcmpb 23568 xkoptsub 23578 xkofvcn 23608 imasnopn 23614 imasncld 23615 imasncls 23616 qtopcmplem 23631 qtopkgen 23634 hmeof1o 23688 hmeores 23695 hmphindis 23721 cmphaushmeo 23724 txhmeo 23727 ptunhmeo 23732 hausflim 23905 flfneii 23916 hausflf 23921 flimfnfcls 23952 flfcntr 23967 cnextfun 23988 cnextfvval 23989 cnextf 23990 cnextcn 23991 cnextfres1 23992 retopon 24700 evth 24905 evth2 24906 qtophaus 33470 rrhre 33655 pconnconn 34874 connpconn 34878 pconnpi1 34880 sconnpi1 34882 txsconnlem 34883 txsconn 34884 cvmsf1o 34915 cvmliftmolem1 34924 cvmliftlem8 34935 cvmlift2lem9a 34946 cvmlift2lem9 34954 cvmlift2lem11 34956 cvmlift2lem12 34957 cvmliftphtlem 34960 cvmlift3lem6 34967 cvmlift3lem8 34969 cvmlift3lem9 34970 cnres2 37269 cnresima 37270 hausgraph 42664 ntrf2 43585 fcnre 44418 |
Copyright terms: Public domain | W3C validator |