Metamath Proof Explorer

Theorem fbunfip

Description: A helpful lemma for showing that certain sets generate filters. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbunfip 
|- ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` ( F u. G ) ) <-> A. x e. F A. y e. G ( x i^i y ) =/= (/) ) )

Proof

Step Hyp Ref Expression
1 elfiun 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( (/) e. ( fi ` ( F u. G ) ) <-> ( (/) e. ( fi ` F ) \/ (/) e. ( fi ` G ) \/ E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) ) )
2 1 notbid 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` ( F u. G ) ) <-> -. ( (/) e. ( fi ` F ) \/ (/) e. ( fi ` G ) \/ E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) ) )
3 3ioran 
 |-  ( -. ( (/) e. ( fi ` F ) \/ (/) e. ( fi ` G ) \/ E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) <-> ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) )
4 df-3an 
 |-  ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) <-> ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) )
5 3 4 bitr2i 
 |-  ( ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) <-> -. ( (/) e. ( fi ` F ) \/ (/) e. ( fi ` G ) \/ E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) )
6 2 5 syl6bbr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` ( F u. G ) ) <-> ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) ) )
7 nesym 
 |-  ( ( x i^i y ) =/= (/) <-> -. (/) = ( x i^i y ) )
8 7 ralbii 
 |-  ( A. y e. ( fi ` G ) ( x i^i y ) =/= (/) <-> A. y e. ( fi ` G ) -. (/) = ( x i^i y ) )
9 ralnex 
 |-  ( A. y e. ( fi ` G ) -. (/) = ( x i^i y ) <-> -. E. y e. ( fi ` G ) (/) = ( x i^i y ) )
10 8 9 bitri 
 |-  ( A. y e. ( fi ` G ) ( x i^i y ) =/= (/) <-> -. E. y e. ( fi ` G ) (/) = ( x i^i y ) )
11 10 ralbii 
 |-  ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) <-> A. x e. ( fi ` F ) -. E. y e. ( fi ` G ) (/) = ( x i^i y ) )
12 ralnex 
 |-  ( A. x e. ( fi ` F ) -. E. y e. ( fi ` G ) (/) = ( x i^i y ) <-> -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) )
13 11 12 bitri 
 |-  ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) <-> -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) )
14 fbasfip 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. ( fi ` F ) )
15 fbasfip 
 |-  ( G e. ( fBas ` Y ) -> -. (/) e. ( fi ` G ) )
16 14 15 anim12i 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) )
17 16 biantrurd 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) <-> ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) ) )
18 13 17 syl5rbb 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( ( ( -. (/) e. ( fi ` F ) /\ -. (/) e. ( fi ` G ) ) /\ -. E. x e. ( fi ` F ) E. y e. ( fi ` G ) (/) = ( x i^i y ) ) <-> A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) ) )
19 ssfii 
 |-  ( F e. ( fBas ` X ) -> F C_ ( fi ` F ) )
20 ssralv 
 |-  ( F C_ ( fi ` F ) -> ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. x e. F A. y e. ( fi ` G ) ( x i^i y ) =/= (/) ) )
21 19 20 syl 
 |-  ( F e. ( fBas ` X ) -> ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. x e. F A. y e. ( fi ` G ) ( x i^i y ) =/= (/) ) )
22 ssfii 
 |-  ( G e. ( fBas ` Y ) -> G C_ ( fi ` G ) )
23 ssralv 
 |-  ( G C_ ( fi ` G ) -> ( A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. y e. G ( x i^i y ) =/= (/) ) )
24 22 23 syl 
 |-  ( G e. ( fBas ` Y ) -> ( A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. y e. G ( x i^i y ) =/= (/) ) )
25 24 ralimdv 
 |-  ( G e. ( fBas ` Y ) -> ( A. x e. F A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. x e. F A. y e. G ( x i^i y ) =/= (/) ) )
26 21 25 sylan9 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) -> A. x e. F A. y e. G ( x i^i y ) =/= (/) ) )
27 ineq1 
 |-  ( x = z -> ( x i^i y ) = ( z i^i y ) )
28 27 neeq1d 
 |-  ( x = z -> ( ( x i^i y ) =/= (/) <-> ( z i^i y ) =/= (/) ) )
29 ineq2 
 |-  ( y = w -> ( z i^i y ) = ( z i^i w ) )
30 29 neeq1d 
 |-  ( y = w -> ( ( z i^i y ) =/= (/) <-> ( z i^i w ) =/= (/) ) )
31 28 30 cbvral2vw 
 |-  ( A. x e. F A. y e. G ( x i^i y ) =/= (/) <-> A. z e. F A. w e. G ( z i^i w ) =/= (/) )
32 fbssfi 
 |-  ( ( F e. ( fBas ` X ) /\ x e. ( fi ` F ) ) -> E. z e. F z C_ x )
33 fbssfi 
 |-  ( ( G e. ( fBas ` Y ) /\ y e. ( fi ` G ) ) -> E. w e. G w C_ y )
34 r19.29 
 |-  ( ( A. z e. F A. w e. G ( z i^i w ) =/= (/) /\ E. z e. F z C_ x ) -> E. z e. F ( A. w e. G ( z i^i w ) =/= (/) /\ z C_ x ) )
35 r19.29 
 |-  ( ( A. w e. G ( z i^i w ) =/= (/) /\ E. w e. G w C_ y ) -> E. w e. G ( ( z i^i w ) =/= (/) /\ w C_ y ) )
36 ss2in 
 |-  ( ( z C_ x /\ w C_ y ) -> ( z i^i w ) C_ ( x i^i y ) )
37 sseq2 
 |-  ( ( x i^i y ) = (/) -> ( ( z i^i w ) C_ ( x i^i y ) <-> ( z i^i w ) C_ (/) ) )
38 ss0 
 |-  ( ( z i^i w ) C_ (/) -> ( z i^i w ) = (/) )
39 37 38 syl6bi 
 |-  ( ( x i^i y ) = (/) -> ( ( z i^i w ) C_ ( x i^i y ) -> ( z i^i w ) = (/) ) )
40 36 39 syl5com 
 |-  ( ( z C_ x /\ w C_ y ) -> ( ( x i^i y ) = (/) -> ( z i^i w ) = (/) ) )
41 40 necon3d 
 |-  ( ( z C_ x /\ w C_ y ) -> ( ( z i^i w ) =/= (/) -> ( x i^i y ) =/= (/) ) )
42 41 ex 
 |-  ( z C_ x -> ( w C_ y -> ( ( z i^i w ) =/= (/) -> ( x i^i y ) =/= (/) ) ) )
43 42 com13 
 |-  ( ( z i^i w ) =/= (/) -> ( w C_ y -> ( z C_ x -> ( x i^i y ) =/= (/) ) ) )
44 43 imp 
 |-  ( ( ( z i^i w ) =/= (/) /\ w C_ y ) -> ( z C_ x -> ( x i^i y ) =/= (/) ) )
45 44 rexlimivw 
 |-  ( E. w e. G ( ( z i^i w ) =/= (/) /\ w C_ y ) -> ( z C_ x -> ( x i^i y ) =/= (/) ) )
46 35 45 syl 
 |-  ( ( A. w e. G ( z i^i w ) =/= (/) /\ E. w e. G w C_ y ) -> ( z C_ x -> ( x i^i y ) =/= (/) ) )
47 46 impancom 
 |-  ( ( A. w e. G ( z i^i w ) =/= (/) /\ z C_ x ) -> ( E. w e. G w C_ y -> ( x i^i y ) =/= (/) ) )
48 47 rexlimivw 
 |-  ( E. z e. F ( A. w e. G ( z i^i w ) =/= (/) /\ z C_ x ) -> ( E. w e. G w C_ y -> ( x i^i y ) =/= (/) ) )
49 34 48 syl 
 |-  ( ( A. z e. F A. w e. G ( z i^i w ) =/= (/) /\ E. z e. F z C_ x ) -> ( E. w e. G w C_ y -> ( x i^i y ) =/= (/) ) )
50 49 expimpd 
 |-  ( A. z e. F A. w e. G ( z i^i w ) =/= (/) -> ( ( E. z e. F z C_ x /\ E. w e. G w C_ y ) -> ( x i^i y ) =/= (/) ) )
51 50 com12 
 |-  ( ( E. z e. F z C_ x /\ E. w e. G w C_ y ) -> ( A. z e. F A. w e. G ( z i^i w ) =/= (/) -> ( x i^i y ) =/= (/) ) )
52 32 33 51 syl2an 
 |-  ( ( ( F e. ( fBas ` X ) /\ x e. ( fi ` F ) ) /\ ( G e. ( fBas ` Y ) /\ y e. ( fi ` G ) ) ) -> ( A. z e. F A. w e. G ( z i^i w ) =/= (/) -> ( x i^i y ) =/= (/) ) )
53 52 an4s 
 |-  ( ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) /\ ( x e. ( fi ` F ) /\ y e. ( fi ` G ) ) ) -> ( A. z e. F A. w e. G ( z i^i w ) =/= (/) -> ( x i^i y ) =/= (/) ) )
54 53 ralrimdvva 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( A. z e. F A. w e. G ( z i^i w ) =/= (/) -> A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) ) )
55 31 54 syl5bi 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( A. x e. F A. y e. G ( x i^i y ) =/= (/) -> A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) ) )
56 26 55 impbid 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( A. x e. ( fi ` F ) A. y e. ( fi ` G ) ( x i^i y ) =/= (/) <-> A. x e. F A. y e. G ( x i^i y ) =/= (/) ) )
57 6 18 56 3bitrd 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` Y ) ) -> ( -. (/) e. ( fi ` ( F u. G ) ) <-> A. x e. F A. y e. G ( x i^i y ) =/= (/) ) )