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

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