![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > toponmax | Structured version Visualization version GIF version |
Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toponmax | ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toponuni 22397 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
2 | topontop 22396 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | |
3 | eqid 2733 | . . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
4 | 3 | topopn 22389 | . . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽) |
5 | 2, 4 | syl 17 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽) |
6 | 1, 5 | eqeltrd 2834 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∪ cuni 4906 ‘cfv 6539 Topctop 22376 TopOnctopon 22393 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5297 ax-nul 5304 ax-pow 5361 ax-pr 5425 ax-un 7719 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4527 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4907 df-br 5147 df-opab 5209 df-mpt 5230 df-id 5572 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-iota 6491 df-fun 6541 df-fv 6547 df-top 22377 df-topon 22394 |
This theorem is referenced by: topgele 22413 eltpsg 22426 eltpsgOLD 22427 en2top 22469 resttopon 22646 ordtrest 22687 ordtrest2lem 22688 ordtrest2 22689 lmfval 22717 cnpfval 22719 iscn 22720 iscnp 22722 lmbrf 22745 cncls 22759 cnconst2 22768 cnrest2 22771 cndis 22776 cnindis 22777 cnpdis 22778 lmfss 22781 lmres 22785 lmff 22786 ist1-3 22834 connsuba 22905 unconn 22914 kgenval 23020 elkgen 23021 kgentopon 23023 pttoponconst 23082 tx1cn 23094 tx2cn 23095 ptcls 23101 xkoccn 23104 txlm 23133 cnmpt2res 23162 xkoinjcn 23172 qtoprest 23202 ordthmeolem 23286 pt1hmeo 23291 xkocnv 23299 flimclslem 23469 flfval 23475 flfnei 23476 isflf 23478 flfcnp 23489 txflf 23491 supnfcls 23505 fclscf 23510 fclscmp 23515 fcfval 23518 isfcf 23519 uffcfflf 23524 cnpfcf 23526 mopnm 23931 isxms2 23935 prdsxmslem2 24019 bcth2 24828 dvmptid 25455 dvmptc 25456 dvtaylp 25863 taylthlem1 25866 taylthlem2 25867 pige3ALT 26010 dvcxp1 26227 cxpcn3 26235 ordtrestNEW 32838 ordtrest2NEWlem 32839 ordtrest2NEW 32840 topjoin 35187 areacirclem1 36513 |
Copyright terms: Public domain | W3C validator |