Theorem topbas

Description: A topology is its own basis. (Contributed by NM, 17-Jul-2006)

	Ref	Expression
Assertion	topbas	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ TopBases )

Proof

Step	Hyp	Ref	Expression
1		inopn	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
2	1	3expb	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 )
3		simpr	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) )
4		ssid	⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
5	3 4	jctir	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6		eleq2	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
7		sseq1	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
8	6 7	anbi12d	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9	8	rspcev	⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐽 ∧ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
10	2 5 9	syl2an2r	⊢ ( ( ( 𝐽 ∈ Top ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
11	10	exp31	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
12	11	ralrimdv	⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
13	12	ralrimivv	⊢ ( 𝐽 ∈ Top → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
14		isbasis2g	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐽 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
15	13 14	mpbird	⊢ ( 𝐽 ∈ Top → 𝐽 ∈ TopBases )