This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑋 ) ∧ 𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )