Theorem fbasssin

Description: A filter base contains subsets of its pairwise intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Jeff Hankins, 1-Dec-2010)

	Ref	Expression
Assertion	fbasssin	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
2		isfbas2	⊢ ( 𝑋 ∈ dom fBas → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ) ) )
3	1 2	syl	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ) ) )
4	3	ibi	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) ) )
5	4	simprd	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ) )
6	5	simp3d	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) )
7		ineq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∩ 𝑧 ) = ( 𝐴 ∩ 𝑧 ) )
8	7	sseq2d	⊢ ( 𝑦 = 𝐴 → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝑧 ) ) )
9	8	rexbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝑧 ) ) )
10		ineq2	⊢ ( 𝑧 = 𝐵 → ( 𝐴 ∩ 𝑧 ) = ( 𝐴 ∩ 𝐵 ) )
11	10	sseq2d	⊢ ( 𝑧 = 𝐵 → ( 𝑥 ⊆ ( 𝐴 ∩ 𝑧 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
12	11	rexbidv	⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝑧 ) ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
13	9 12	rspc2v	⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ( ∀ 𝑦 ∈ 𝐹 ∀ 𝑧 ∈ 𝐹 ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
14	6 13	syl5com	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
15	14	3impib	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )