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 
|- ( ( F e. ( fBas ` B ) /\ S e. F /\ S e. Fin ) -> |^| F =/= (/) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = y -> ( x e. F <-> y e. F ) )
2 1 anbi2d 
 |-  ( x = y -> ( ( F e. ( fBas ` B ) /\ x e. F ) <-> ( F e. ( fBas ` B ) /\ y e. F ) ) )
3 2 imbi1d 
 |-  ( x = y -> ( ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) <-> ( ( F e. ( fBas ` B ) /\ y e. F ) -> |^| F =/= (/) ) ) )
4 eleq1 
 |-  ( x = S -> ( x e. F <-> S e. F ) )
5 4 anbi2d 
 |-  ( x = S -> ( ( F e. ( fBas ` B ) /\ x e. F ) <-> ( F e. ( fBas ` B ) /\ S e. F ) ) )
6 5 imbi1d 
 |-  ( x = S -> ( ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) <-> ( ( F e. ( fBas ` B ) /\ S e. F ) -> |^| F =/= (/) ) ) )
7 bi2.04 
 |-  ( ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) <-> ( ( F e. ( fBas ` B ) /\ x e. F ) -> ( x C. y -> |^| F =/= (/) ) ) )
8 ibar 
 |-  ( F e. ( fBas ` B ) -> ( x e. F <-> ( F e. ( fBas ` B ) /\ x e. F ) ) )
9 8 adantr 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( x e. F <-> ( F e. ( fBas ` B ) /\ x e. F ) ) )
10 9 imbi1d 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( ( x e. F -> ( x C. y -> |^| F =/= (/) ) ) <-> ( ( F e. ( fBas ` B ) /\ x e. F ) -> ( x C. y -> |^| F =/= (/) ) ) ) )
11 7 10 bitr4id 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) <-> ( x e. F -> ( x C. y -> |^| F =/= (/) ) ) ) )
12 11 albidv 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( A. x ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) <-> A. x ( x e. F -> ( x C. y -> |^| F =/= (/) ) ) ) )
13 df-ral 
 |-  ( A. x e. F ( x C. y -> |^| F =/= (/) ) <-> A. x ( x e. F -> ( x C. y -> |^| F =/= (/) ) ) )
14 12 13 bitr4di 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( A. x ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) <-> A. x e. F ( x C. y -> |^| F =/= (/) ) ) )
15 0nelfb 
 |-  ( F e. ( fBas ` B ) -> -. (/) e. F )
16 eleq1 
 |-  ( y = (/) -> ( y e. F <-> (/) e. F ) )
17 16 notbid 
 |-  ( y = (/) -> ( -. y e. F <-> -. (/) e. F ) )
18 15 17 syl5ibrcom 
 |-  ( F e. ( fBas ` B ) -> ( y = (/) -> -. y e. F ) )
19 18 necon2ad 
 |-  ( F e. ( fBas ` B ) -> ( y e. F -> y =/= (/) ) )
20 19 imp 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> y =/= (/) )
21 ssn0 
 |-  ( ( y C_ |^| F /\ y =/= (/) ) -> |^| F =/= (/) )
22 21 ex 
 |-  ( y C_ |^| F -> ( y =/= (/) -> |^| F =/= (/) ) )
23 20 22 syl5com 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( y C_ |^| F -> |^| F =/= (/) ) )
24 23 a1dd 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( y C_ |^| F -> ( A. x e. F ( x C. y -> |^| F =/= (/) ) -> |^| F =/= (/) ) ) )
25 ssint 
 |-  ( y C_ |^| F <-> A. z e. F y C_ z )
26 25 notbii 
 |-  ( -. y C_ |^| F <-> -. A. z e. F y C_ z )
27 rexnal 
 |-  ( E. z e. F -. y C_ z <-> -. A. z e. F y C_ z )
28 26 27 bitr4i 
 |-  ( -. y C_ |^| F <-> E. z e. F -. y C_ z )
29 fbasssin 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F /\ z e. F ) -> E. x e. F x C_ ( y i^i z ) )
30 nssinpss 
 |-  ( -. y C_ z <-> ( y i^i z ) C. y )
31 sspsstr 
 |-  ( ( x C_ ( y i^i z ) /\ ( y i^i z ) C. y ) -> x C. y )
32 30 31 sylan2b 
 |-  ( ( x C_ ( y i^i z ) /\ -. y C_ z ) -> x C. y )
33 32 expcom 
 |-  ( -. y C_ z -> ( x C_ ( y i^i z ) -> x C. y ) )
34 33 reximdv 
 |-  ( -. y C_ z -> ( E. x e. F x C_ ( y i^i z ) -> E. x e. F x C. y ) )
35 29 34 syl5com 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F /\ z e. F ) -> ( -. y C_ z -> E. x e. F x C. y ) )
36 35 3expia 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( z e. F -> ( -. y C_ z -> E. x e. F x C. y ) ) )
37 36 rexlimdv 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( E. z e. F -. y C_ z -> E. x e. F x C. y ) )
38 28 37 syl5bi 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( -. y C_ |^| F -> E. x e. F x C. y ) )
39 r19.29 
 |-  ( ( A. x e. F ( x C. y -> |^| F =/= (/) ) /\ E. x e. F x C. y ) -> E. x e. F ( ( x C. y -> |^| F =/= (/) ) /\ x C. y ) )
40 id 
 |-  ( ( x C. y -> |^| F =/= (/) ) -> ( x C. y -> |^| F =/= (/) ) )
41 40 imp 
 |-  ( ( ( x C. y -> |^| F =/= (/) ) /\ x C. y ) -> |^| F =/= (/) )
42 41 rexlimivw 
 |-  ( E. x e. F ( ( x C. y -> |^| F =/= (/) ) /\ x C. y ) -> |^| F =/= (/) )
43 39 42 syl 
 |-  ( ( A. x e. F ( x C. y -> |^| F =/= (/) ) /\ E. x e. F x C. y ) -> |^| F =/= (/) )
44 43 expcom 
 |-  ( E. x e. F x C. y -> ( A. x e. F ( x C. y -> |^| F =/= (/) ) -> |^| F =/= (/) ) )
45 38 44 syl6 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( -. y C_ |^| F -> ( A. x e. F ( x C. y -> |^| F =/= (/) ) -> |^| F =/= (/) ) ) )
46 24 45 pm2.61d 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( A. x e. F ( x C. y -> |^| F =/= (/) ) -> |^| F =/= (/) ) )
47 14 46 sylbid 
 |-  ( ( F e. ( fBas ` B ) /\ y e. F ) -> ( A. x ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) -> |^| F =/= (/) ) )
48 47 com12 
 |-  ( A. x ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) -> ( ( F e. ( fBas ` B ) /\ y e. F ) -> |^| F =/= (/) ) )
49 48 a1i 
 |-  ( y e. Fin -> ( A. x ( x C. y -> ( ( F e. ( fBas ` B ) /\ x e. F ) -> |^| F =/= (/) ) ) -> ( ( F e. ( fBas ` B ) /\ y e. F ) -> |^| F =/= (/) ) ) )
50 3 6 49 findcard3 
 |-  ( S e. Fin -> ( ( F e. ( fBas ` B ) /\ S e. F ) -> |^| F =/= (/) ) )
51 50 com12 
 |-  ( ( F e. ( fBas ` B ) /\ S e. F ) -> ( S e. Fin -> |^| F =/= (/) ) )
52 51 3impia 
 |-  ( ( F e. ( fBas ` B ) /\ S e. F /\ S e. Fin ) -> |^| F =/= (/) )