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 ⊢ F ∈ fBas ⁡ X ∧ A ∈ F ∧ B ∈ F → ∃ x ∈ F x ⊆ A ∩ B

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ F ∈ fBas ⁡ X → X ∈ dom ⁡ fBas
2 isfbas2 ⊢ X ∈ dom ⁡ fBas → F ∈ fBas ⁡ X ↔ F ⊆ 𝒫 X ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z
3 1 2 syl ⊢ F ∈ fBas ⁡ X → F ∈ fBas ⁡ X ↔ F ⊆ 𝒫 X ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z
4 3 ibi ⊢ F ∈ fBas ⁡ X → F ⊆ 𝒫 X ∧ F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z
5 4 simprd ⊢ F ∈ fBas ⁡ X → F ≠ ∅ ∧ ∅ ∉ F ∧ ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z
6 5 simp3d ⊢ F ∈ fBas ⁡ X → ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z
7 ineq1 ⊢ y = A → y ∩ z = A ∩ z
8 7 sseq2d ⊢ y = A → x ⊆ y ∩ z ↔ x ⊆ A ∩ z
9 8 rexbidv ⊢ y = A → ∃ x ∈ F x ⊆ y ∩ z ↔ ∃ x ∈ F x ⊆ A ∩ z
10 ineq2 ⊢ z = B → A ∩ z = A ∩ B
11 10 sseq2d ⊢ z = B → x ⊆ A ∩ z ↔ x ⊆ A ∩ B
12 11 rexbidv ⊢ z = B → ∃ x ∈ F x ⊆ A ∩ z ↔ ∃ x ∈ F x ⊆ A ∩ B
13 9 12 rspc2v ⊢ A ∈ F ∧ B ∈ F → ∀ y ∈ F ∀ z ∈ F ∃ x ∈ F x ⊆ y ∩ z → ∃ x ∈ F x ⊆ A ∩ B
14 6 13 syl5com ⊢ F ∈ fBas ⁡ X → A ∈ F ∧ B ∈ F → ∃ x ∈ F x ⊆ A ∩ B
15 14 3impib ⊢ F ∈ fBas ⁡ X ∧ A ∈ F ∧ B ∈ F → ∃ x ∈ F x ⊆ A ∩ B