Theorem fbasfip

Description: A filter base has the finite intersection property. (Contributed by Jeff Hankins, 2-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	fbasfip	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ ( fi ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		elin	⊢ ( 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ↔ ( 𝑦 ∈ 𝒫 𝐹 ∧ 𝑦 ∈ Fin ) )
2		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐹 → 𝑦 ⊆ 𝐹 )
3	2	anim1i	⊢ ( ( 𝑦 ∈ 𝒫 𝐹 ∧ 𝑦 ∈ Fin ) → ( 𝑦 ⊆ 𝐹 ∧ 𝑦 ∈ Fin ) )
4	1 3	sylbi	⊢ ( 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) → ( 𝑦 ⊆ 𝐹 ∧ 𝑦 ∈ Fin ) )
5		fbssint	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ⊆ 𝐹 ∧ 𝑦 ∈ Fin ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ∩ 𝑦 )
6	5	3expb	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑦 ⊆ 𝐹 ∧ 𝑦 ∈ Fin ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ∩ 𝑦 )
7	4 6	sylan2	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ∩ 𝑦 )
8		0nelfb	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
9	8	ad2antrr	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ 𝑧 ∈ 𝐹 ) → ¬ ∅ ∈ 𝐹 )
10		eleq1	⊢ ( 𝑧 = ∅ → ( 𝑧 ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
11	10	biimpcd	⊢ ( 𝑧 ∈ 𝐹 → ( 𝑧 = ∅ → ∅ ∈ 𝐹 ) )
12	11	adantl	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ 𝑧 ∈ 𝐹 ) → ( 𝑧 = ∅ → ∅ ∈ 𝐹 ) )
13	9 12	mtod	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ 𝑧 ∈ 𝐹 ) → ¬ 𝑧 = ∅ )
14		ss0	⊢ ( 𝑧 ⊆ ∅ → 𝑧 = ∅ )
15	13 14	nsyl	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ 𝑧 ∈ 𝐹 ) → ¬ 𝑧 ⊆ ∅ )
16	15	adantrr	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ∩ 𝑦 ) ) → ¬ 𝑧 ⊆ ∅ )
17		sseq2	⊢ ( ∅ = ∩ 𝑦 → ( 𝑧 ⊆ ∅ ↔ 𝑧 ⊆ ∩ 𝑦 ) )
18	17	biimprcd	⊢ ( 𝑧 ⊆ ∩ 𝑦 → ( ∅ = ∩ 𝑦 → 𝑧 ⊆ ∅ ) )
19	18	ad2antll	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ∩ 𝑦 ) ) → ( ∅ = ∩ 𝑦 → 𝑧 ⊆ ∅ ) )
20	16 19	mtod	⊢ ( ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) ∧ ( 𝑧 ∈ 𝐹 ∧ 𝑧 ⊆ ∩ 𝑦 ) ) → ¬ ∅ = ∩ 𝑦 )
21	7 20	rexlimddv	⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ) → ¬ ∅ = ∩ 𝑦 )
22	21	nrexdv	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∃ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ∅ = ∩ 𝑦 )
23		0ex	⊢ ∅ ∈ V
24		elfi	⊢ ( ( ∅ ∈ V ∧ 𝐹 ∈ ( fBas ‘ 𝑋 ) ) → ( ∅ ∈ ( fi ‘ 𝐹 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ∅ = ∩ 𝑦 ) )
25	23 24	mpan	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ∅ ∈ ( fi ‘ 𝐹 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐹 ∩ Fin ) ∅ = ∩ 𝑦 ) )
26	22 25	mtbird	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ¬ ∅ ∈ ( fi ‘ 𝐹 ) )