![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > topontopi | Structured version Visualization version GIF version |
Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
topontopi.1 | ⊢ 𝐽 ∈ (TopOn‘𝐵) |
Ref | Expression |
---|---|
topontopi | ⊢ 𝐽 ∈ Top |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topontopi.1 | . 2 ⊢ 𝐽 ∈ (TopOn‘𝐵) | |
2 | topontop 21043 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐽 ∈ Top |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 ‘cfv 6100 Topctop 21023 TopOnctopon 21040 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2776 ax-sep 4974 ax-nul 4982 ax-pow 5034 ax-pr 5096 ax-un 7182 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2785 df-cleq 2791 df-clel 2794 df-nfc 2929 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3386 df-sbc 3633 df-dif 3771 df-un 3773 df-in 3775 df-ss 3782 df-nul 4115 df-if 4277 df-pw 4350 df-sn 4368 df-pr 4370 df-op 4374 df-uni 4628 df-br 4843 df-opab 4905 df-mpt 4922 df-id 5219 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-iota 6063 df-fun 6102 df-fv 6108 df-topon 21041 |
This theorem is referenced by: sn0top 21129 indistop 21132 letop 21336 dfac14 21747 cnfldtop 22912 sszcld 22945 iitop 23008 limccnp2 23994 cxpcn3 24830 lmlim 30502 pnfneige0 30506 sxbrsigalem4 30858 knoppcnlem10 32993 poimir 33924 islptre 40584 fourierdlem62 41117 |
Copyright terms: Public domain | W3C validator |