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