toponunii - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > toponunii		Structured version Visualization version GIF version

Theorem toponunii 22836

Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)

**Hypothesis**
Ref	Expression
topontopi.1	⊢ 𝐽 ∈ (TopOn‘𝐵)

**Assertion**
Ref	Expression
toponunii	⊢ 𝐵 = ∪ 𝐽

**Proof of Theorem toponunii**
Step	Hyp	Ref	Expression
1		topontopi.1	. 2 ⊢ 𝐽 ∈ (TopOn‘𝐵)
2		toponuni 22834	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)
3	1, 2	ax-mp 5	1 ⊢ 𝐵 = ∪ 𝐽

Colors of variables: wff setvar class

Syntax hints: = wceq 1533 ∈ wcel 2098 ∪ cuni 4910 ‘cfv 6551 TopOnctopon 22830

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 2698 ax-sep 5301 ax-nul 5308 ax-pow 5367 ax-pr 5431 ax-un 7744

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 2705 df-cleq 2719 df-clel 2805 df-nfc 2880 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4325 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4911 df-br 5151 df-opab 5213 df-mpt 5234 df-id 5578 df-xp 5686 df-rel 5687 df-cnv 5688 df-co 5689 df-dm 5690 df-iota 6503 df-fun 6553 df-fv 6559 df-topon 22831

This theorem is referenced by: toponrestid 22841 indisuni 22924 indistpsx 22931 letopuni 23129 dfac14 23540 unicntop 24720 sszcld 24751 reperflem 24752 cnperf 24754 iiuni 24819 abscncfALT 24863 cncfcnvcn 24864 cnheiborlem 24898 cnheibor 24899 cnllycmp 24900 bndth 24902 mbfimaopnlem 25602 limcnlp 25825 limcflflem 25827 limcflf 25828 limcmo 25829 limcres 25833 limccnp 25838 limccnp2 25839 perfdvf 25850 recnperf 25852 dvcnp2 25867 dvcnp2OLD 25868 dvaddbr 25886 dvmulbr 25887 dvmulbrOLD 25888 dvcobr 25895 dvcobrOLD 25896 dvcnvlem 25926 lhop1lem 25964 taylthlem2 26327 taylthlem2OLD 26328 abelth 26396 cxpcn3 26701 lgamucov 26988 ftalem3 27025 blocni 30633 ipasslem8 30665 ubthlem1 30698 tpr2uni 33511 tpr2rico 33518 mndpluscn 33532 raddcn 33535 cvxsconn 34858 cvmlift2lem11 34928 ivthALT 35824 poimir 37131 broucube 37132 dvtanlem 37147 ftc1cnnc 37170 dvasin 37182 dvacos 37183 dvreasin 37184 dvreacos 37185 areacirclem2 37187 reheibor 37317 islptre 45009 dirkercncf 45497 fourierdlem62 45558

	
		OSZAR »