toptopon2 - Metamath Proof Explorer

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

Theorem toptopon2 22833

Description: A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.)

**Assertion**
Ref	Expression
toptopon2	⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

**Proof of Theorem toptopon2**
Step	Hyp	Ref	Expression
1		eqid 2728	. 2 ⊢ ∪ 𝐽 = ∪ 𝐽
2	1	toptopon 22832	1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽))

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∈ wcel 2099 ∪ cuni 4908 ‘cfv 6548 Topctop 22808 TopOnctopon 22825

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-sep 5299 ax-nul 5306 ax-pow 5365 ax-pr 5429 ax-un 7740

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ral 3059 df-rex 3068 df-rab 3430 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-iota 6500 df-fun 6550 df-fv 6556 df-topon 22826

This theorem is referenced by: topontopon 22834 toprntopon 22840 neiptopreu 23050 lmcvg 23179 cnss1 23193 cnss2 23194 cnrest2 23203 cnrest2r 23204 lmss 23215 lmcnp 23221 lmcn 23222 t1t0 23265 haust1 23269 restcnrm 23279 resthauslem 23280 lmmo 23297 rncmp 23313 connima 23342 conncn 23343 kgeni 23454 kgenftop 23457 kgenss 23460 kgenhaus 23461 kgencmp2 23463 kgenidm 23464 1stckgen 23471 kgencn3 23475 kgen2cn 23476 dfac14 23535 ptcnplem 23538 ptcnp 23539 txcnmpt 23541 ptcn 23544 txdis1cn 23552 lmcn2 23566 txkgen 23569 xkohaus 23570 xkopt 23572 cnmpt11 23580 cnmpt11f 23581 cnmpt1t 23582 cnmpt12 23584 cnmpt21 23588 cnmpt21f 23589 cnmpt2t 23590 cnmpt22 23591 cnmpt22f 23592 cnmptcom 23595 cnmptkp 23597 cnmpt2k 23605 txconn 23606 qtopss 23632 qtopeu 23633 qtopomap 23635 qtopcmap 23636 kqtop 23662 kqt0 23663 nrmr0reg 23666 regr1 23667 kqreg 23668 kqnrm 23669 hmeoqtop 23692 hmphref 23698 xpstopnlem1 23726 ptcmpfi 23730 xkocnv 23731 xkohmeo 23732 kqhmph 23736 flimsncls 23903 cnpflfi 23916 flfcnp 23921 flfcnp2 23924 cnpfcfi 23957 cnextucn 24221 cnmpopc 24862 htpyco1 24917 htpyco2 24918 phtpyco2 24929 pcopt 24962 pcopt2 24963 pcorevlem 24966 pi1cof 24999 pi1coghm 25001 cvxsconn 34853 clduni 47919

	
		OSZAR »