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

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 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ∩ 𝐴 )