Metamath Proof Explorer


Theorem fbssint

Description: A filter base contains subsets of its finite intersections. (Contributed by Jeff Hankins, 1-Sep-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbssint ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) → ∃ 𝑥𝐹 𝑥 𝐴 )

Proof

Step Hyp Ref Expression
1 fbasne0 ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → 𝐹 ≠ ∅ )
2 n0 ( 𝐹 ≠ ∅ ↔ ∃ 𝑥 𝑥𝐹 )
3 1 2 sylib ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ∃ 𝑥 𝑥𝐹 )
4 ssv 𝑥 ⊆ V
5 4 jctr ( 𝑥𝐹 → ( 𝑥𝐹𝑥 ⊆ V ) )
6 5 eximi ( ∃ 𝑥 𝑥𝐹 → ∃ 𝑥 ( 𝑥𝐹𝑥 ⊆ V ) )
7 df-rex ( ∃ 𝑥𝐹 𝑥 ⊆ V ↔ ∃ 𝑥 ( 𝑥𝐹𝑥 ⊆ V ) )
8 6 7 sylibr ( ∃ 𝑥 𝑥𝐹 → ∃ 𝑥𝐹 𝑥 ⊆ V )
9 3 8 syl ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ∃ 𝑥𝐹 𝑥 ⊆ V )
10 inteq ( 𝐴 = ∅ → 𝐴 = ∅ )
11 int0 ∅ = V
12 10 11 eqtrdi ( 𝐴 = ∅ → 𝐴 = V )
13 12 sseq2d ( 𝐴 = ∅ → ( 𝑥 𝐴𝑥 ⊆ V ) )
14 13 rexbidv ( 𝐴 = ∅ → ( ∃ 𝑥𝐹 𝑥 𝐴 ↔ ∃ 𝑥𝐹 𝑥 ⊆ V ) )
15 9 14 syl5ibrcom ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝐴 = ∅ → ∃ 𝑥𝐹 𝑥 𝐴 ) )
16 15 3ad2ant1 ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) → ( 𝐴 = ∅ → ∃ 𝑥𝐹 𝑥 𝐴 ) )
17 simpl1 ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐹 ∈ ( fBas ‘ 𝐵 ) )
18 simpl2 ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴𝐹 )
19 simpr ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
20 simpl3 ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ Fin )
21 elfir ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ ( 𝐴𝐹𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ ( fi ‘ 𝐹 ) )
22 17 18 19 20 21 syl13anc ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ ( fi ‘ 𝐹 ) )
23 fbssfi ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴 ∈ ( fi ‘ 𝐹 ) ) → ∃ 𝑥𝐹 𝑥 𝐴 )
24 17 22 23 syl2anc ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥𝐹 𝑥 𝐴 )
25 24 ex ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) → ( 𝐴 ≠ ∅ → ∃ 𝑥𝐹 𝑥 𝐴 ) )
26 16 25 pm2.61dne ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝐴𝐹𝐴 ∈ Fin ) → ∃ 𝑥𝐹 𝑥 𝐴 )