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