Metamath Proof Explorer

Theorem fbfinnfr

Description: No filter base containing a finite element is free. (Contributed by Jeff Hankins, 5-Dec-2009) (Revised by Stefan O'Rear, 28-Jul-2015)

Ref Expression
Assertion fbfinnfr ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin ) → ∩ 𝐹 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐹 ↔ 𝑦 ∈ 𝐹 ) )
2 1 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) ) )
3 2 imbi1d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ↔ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) )
4 eleq1 ⊢ ( 𝑥 = 𝑆 → ( 𝑥 ∈ 𝐹 ↔ 𝑆 ∈ 𝐹 ) )
5 4 anbi2d ⊢ ( 𝑥 = 𝑆 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ) ) )
6 5 imbi1d ⊢ ( 𝑥 = 𝑆 → ( ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ↔ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) )
7 bi2.04 ⊢ ( ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) ↔ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) )
8 ibar ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) ) )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∈ 𝐹 ↔ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) ) )
10 9 imbi1d ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) ↔ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) ) )
11 7 10 bitr4id ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) ↔ ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) ) )
12 11 albidv ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) ) )
13 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐹 → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) )
14 12 13 bitr4di ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) ↔ ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ) )
15 0nelfb ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ¬ ∅ ∈ 𝐹 )
16 eleq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ∈ 𝐹 ↔ ∅ ∈ 𝐹 ) )
17 16 notbid ⊢ ( 𝑦 = ∅ → ( ¬ 𝑦 ∈ 𝐹 ↔ ¬ ∅ ∈ 𝐹 ) )
18 15 17 syl5ibrcom ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝑦 = ∅ → ¬ 𝑦 ∈ 𝐹 ) )
19 18 necon2ad ⊢ ( 𝐹 ∈ ( fBas ‘ 𝐵 ) → ( 𝑦 ∈ 𝐹 → 𝑦 ≠ ∅ ) )
20 19 imp ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → 𝑦 ≠ ∅ )
21 ssn0 ⊢ ( ( 𝑦 ⊆ ∩ 𝐹 ∧ 𝑦 ≠ ∅ ) → ∩ 𝐹 ≠ ∅ )
22 21 ex ⊢ ( 𝑦 ⊆ ∩ 𝐹 → ( 𝑦 ≠ ∅ → ∩ 𝐹 ≠ ∅ ) )
23 20 22 syl5com ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 ⊆ ∩ 𝐹 → ∩ 𝐹 ≠ ∅ ) )
24 23 a1dd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑦 ⊆ ∩ 𝐹 → ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≠ ∅ ) ) )
25 ssint ⊢ ( 𝑦 ⊆ ∩ 𝐹 ↔ ∀ 𝑧 ∈ 𝐹 𝑦 ⊆ 𝑧 )
26 25 notbii ⊢ ( ¬ 𝑦 ⊆ ∩ 𝐹 ↔ ¬ ∀ 𝑧 ∈ 𝐹 𝑦 ⊆ 𝑧 )
27 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐹 ¬ 𝑦 ⊆ 𝑧 ↔ ¬ ∀ 𝑧 ∈ 𝐹 𝑦 ⊆ 𝑧 )
28 26 27 bitr4i ⊢ ( ¬ 𝑦 ⊆ ∩ 𝐹 ↔ ∃ 𝑧 ∈ 𝐹 ¬ 𝑦 ⊆ 𝑧 )
29 fbasssin ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) )
30 nssinpss ⊢ ( ¬ 𝑦 ⊆ 𝑧 ↔ ( 𝑦 ∩ 𝑧 ) ⊊ 𝑦 )
31 sspsstr ⊢ ( ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ∧ ( 𝑦 ∩ 𝑧 ) ⊊ 𝑦 ) → 𝑥 ⊊ 𝑦 )
32 30 31 sylan2b ⊢ ( ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) ∧ ¬ 𝑦 ⊆ 𝑧 ) → 𝑥 ⊊ 𝑦 )
33 32 expcom ⊢ ( ¬ 𝑦 ⊆ 𝑧 → ( 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → 𝑥 ⊊ 𝑦 ) )
34 33 reximdv ⊢ ( ¬ 𝑦 ⊆ 𝑧 → ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ ( 𝑦 ∩ 𝑧 ) → ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) )
35 29 34 syl5com ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ∧ 𝑧 ∈ 𝐹 ) → ( ¬ 𝑦 ⊆ 𝑧 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) )
36 35 3expia ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑧 ∈ 𝐹 → ( ¬ 𝑦 ⊆ 𝑧 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) ) )
37 36 rexlimdv ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ∃ 𝑧 ∈ 𝐹 ¬ 𝑦 ⊆ 𝑧 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) )
38 28 37 syl5bi ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ¬ 𝑦 ⊆ ∩ 𝐹 → ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) )
39 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) → ∃ 𝑥 ∈ 𝐹 ( ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ∧ 𝑥 ⊊ 𝑦 ) )
40 id ⊢ ( ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) → ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) )
41 40 imp ⊢ ( ( ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ∧ 𝑥 ⊊ 𝑦 ) → ∩ 𝐹 ≠ ∅ )
42 41 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐹 ( ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ∧ 𝑥 ⊊ 𝑦 ) → ∩ 𝐹 ≠ ∅ )
43 39 42 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 ) → ∩ 𝐹 ≠ ∅ )
44 43 expcom ⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊊ 𝑦 → ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≠ ∅ ) )
45 38 44 syl6 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ¬ 𝑦 ⊆ ∩ 𝐹 → ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≠ ∅ ) ) )
46 24 45 pm2.61d ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ∀ 𝑥 ∈ 𝐹 ( 𝑥 ⊊ 𝑦 → ∩ 𝐹 ≠ ∅ ) → ∩ 𝐹 ≠ ∅ ) )
47 14 46 sylbid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) → ∩ 𝐹 ≠ ∅ ) )
48 47 com12 ⊢ ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) )
49 48 a1i ⊢ ( 𝑦 ∈ Fin → ( ∀ 𝑥 ( 𝑥 ⊊ 𝑦 → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑥 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑦 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) ) )
50 3 6 49 findcard3 ⊢ ( 𝑆 ∈ Fin → ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ) → ∩ 𝐹 ≠ ∅ ) )
51 50 com12 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ) → ( 𝑆 ∈ Fin → ∩ 𝐹 ≠ ∅ ) )
52 51 3impia ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝐵 ) ∧ 𝑆 ∈ 𝐹 ∧ 𝑆 ∈ Fin ) → ∩ 𝐹 ≠ ∅ )