Metamath Proof Explorer


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 ‘ 𝐹 ) )