topgele - Metamath Proof Explorer

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

Theorem topgele 20857

Description: The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.)

**Assertion**
Ref	Expression
topgele	⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋))

**Proof of Theorem topgele**
Step	Hyp	Ref	Expression
1		topontop 20841	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top)
2		0opn 20832	. . . 4 ⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽)
3	1, 2	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ∅ ∈ 𝐽)
4		toponmax 20853	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽)
5		0ex 4898	. . . 4 ⊢ ∅ ∈ V
6		prssg 4458	. . . 4 ⊢ ((∅ ∈ V ∧ 𝑋 ∈ 𝐽) → ((∅ ∈ 𝐽 ∧ 𝑋 ∈ 𝐽) ↔ {∅, 𝑋} ⊆ 𝐽))
7	5, 4, 6	sylancr 698	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ((∅ ∈ 𝐽 ∧ 𝑋 ∈ 𝐽) ↔ {∅, 𝑋} ⊆ 𝐽))
8	3, 4, 7	mpbi2and 994	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → {∅, 𝑋} ⊆ 𝐽)
9		toponuni 20842	. . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽)
10		eqimss2 3764	. . . 4 ⊢ (𝑋 = ∪ 𝐽 → ∪ 𝐽 ⊆ 𝑋)
11	9, 10	syl 17	. . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ∪ 𝐽 ⊆ 𝑋)
12		sspwuni 4719	. . 3 ⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋)
13	11, 12	sylibr 224	. 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ⊆ 𝒫 𝑋)
14	8, 13	jca 555	1 ⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1596 ∈ wcel 2103 Vcvv 3304 ⊆ wss 3680 ∅c0 4023 𝒫 cpw 4266 {cpr 4287 ∪ cuni 4544 ‘cfv 6001 Topctop 20821 TopOnctopon 20838

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ne 2897 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-sbc 3542 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-opab 4821 df-mpt 4838 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-iota 5964 df-fun 6003 df-fv 6009 df-top 20822 df-topon 20839

This theorem is referenced by: topsn 20858 txindis 21560 dissneqlem 33419 ntrf2 38841

W3C validator