Theorem fiinbas

Description: If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	fiinbas	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ) → 𝐵 ∈ TopBases )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
2		eleq2	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) )
3		sseq1	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
4	2 3	anbi12d	⊢ ( 𝑤 = ( 𝑥 ∩ 𝑦 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
5	4	rspcev	⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ∧ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
6	1 5	mpanr2	⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
7	6	ralrimiva	⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
8	7	a1i	⊢ ( 𝐵 ∈ 𝐶 → ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9	8	ralimdv	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
10	9	ralimdv	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
11		isbasis2g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
12	10 11	sylibrd	⊢ ( 𝐵 ∈ 𝐶 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 → 𝐵 ∈ TopBases ) )
13	12	imp	⊢ ( ( 𝐵 ∈ 𝐶 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ∩ 𝑦 ) ∈ 𝐵 ) → 𝐵 ∈ TopBases )