Metamath Proof Explorer

Theorem fbun

Description: A necessary and sufficient condition for the union of two filter bases to also be a filter base. (Contributed by Mario Carneiro, 28-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbun 
|- ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( F u. G ) e. ( fBas ` X ) <-> A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) )

Proof

Step Hyp Ref Expression
1 elun1 
 |-  ( x e. F -> x e. ( F u. G ) )
2 elun2 
 |-  ( y e. G -> y e. ( F u. G ) )
3 1 2 anim12i 
 |-  ( ( x e. F /\ y e. G ) -> ( x e. ( F u. G ) /\ y e. ( F u. G ) ) )
4 fbasssin 
 |-  ( ( ( F u. G ) e. ( fBas ` X ) /\ x e. ( F u. G ) /\ y e. ( F u. G ) ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
5 4 3expb 
 |-  ( ( ( F u. G ) e. ( fBas ` X ) /\ ( x e. ( F u. G ) /\ y e. ( F u. G ) ) ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
6 3 5 sylan2 
 |-  ( ( ( F u. G ) e. ( fBas ` X ) /\ ( x e. F /\ y e. G ) ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
7 6 ralrimivva 
 |-  ( ( F u. G ) e. ( fBas ` X ) -> A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) )
8 fbsspw 
 |-  ( F e. ( fBas ` X ) -> F C_ ~P X )
9 8 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> F C_ ~P X )
10 fbsspw 
 |-  ( G e. ( fBas ` X ) -> G C_ ~P X )
11 10 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> G C_ ~P X )
12 9 11 unssd 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( F u. G ) C_ ~P X )
13 12 a1d 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( F u. G ) C_ ~P X ) )
14 ssun1 
 |-  F C_ ( F u. G )
15 fbasne0 
 |-  ( F e. ( fBas ` X ) -> F =/= (/) )
16 ssn0 
 |-  ( ( F C_ ( F u. G ) /\ F =/= (/) ) -> ( F u. G ) =/= (/) )
17 14 15 16 sylancr 
 |-  ( F e. ( fBas ` X ) -> ( F u. G ) =/= (/) )
18 17 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( F u. G ) =/= (/) )
19 18 a1d 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( F u. G ) =/= (/) ) )
20 0nelfb 
 |-  ( F e. ( fBas ` X ) -> -. (/) e. F )
21 0nelfb 
 |-  ( G e. ( fBas ` X ) -> -. (/) e. G )
22 df-nel 
 |-  ( (/) e/ ( F u. G ) <-> -. (/) e. ( F u. G ) )
23 elun 
 |-  ( (/) e. ( F u. G ) <-> ( (/) e. F \/ (/) e. G ) )
24 23 notbii 
 |-  ( -. (/) e. ( F u. G ) <-> -. ( (/) e. F \/ (/) e. G ) )
25 ioran 
 |-  ( -. ( (/) e. F \/ (/) e. G ) <-> ( -. (/) e. F /\ -. (/) e. G ) )
26 22 24 25 3bitri 
 |-  ( (/) e/ ( F u. G ) <-> ( -. (/) e. F /\ -. (/) e. G ) )
27 26 biimpri 
 |-  ( ( -. (/) e. F /\ -. (/) e. G ) -> (/) e/ ( F u. G ) )
28 20 21 27 syl2an 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> (/) e/ ( F u. G ) )
29 28 a1d 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> (/) e/ ( F u. G ) ) )
30 fbasssin 
 |-  ( ( F e. ( fBas ` X ) /\ x e. F /\ y e. F ) -> E. z e. F z C_ ( x i^i y ) )
31 ssrexv 
 |-  ( F C_ ( F u. G ) -> ( E. z e. F z C_ ( x i^i y ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
32 14 30 31 mpsyl 
 |-  ( ( F e. ( fBas ` X ) /\ x e. F /\ y e. F ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
33 32 3expb 
 |-  ( ( F e. ( fBas ` X ) /\ ( x e. F /\ y e. F ) ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
34 33 ralrimivva 
 |-  ( F e. ( fBas ` X ) -> A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
35 34 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
36 pm3.2 
 |-  ( A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) )
37 35 36 syl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) )
38 r19.26 
 |-  ( A. x e. F ( A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) <-> ( A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
39 ralun 
 |-  ( ( A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
40 39 ralimi 
 |-  ( A. x e. F ( A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. x e. F A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
41 38 40 sylbir 
 |-  ( ( A. x e. F A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. x e. F A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
42 37 41 syl6 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> A. x e. F A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
43 ralcom 
 |-  ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) <-> A. y e. G A. x e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
44 ineq1 
 |-  ( x = w -> ( x i^i y ) = ( w i^i y ) )
45 44 sseq2d 
 |-  ( x = w -> ( z C_ ( x i^i y ) <-> z C_ ( w i^i y ) ) )
46 45 rexbidv 
 |-  ( x = w -> ( E. z e. ( F u. G ) z C_ ( x i^i y ) <-> E. z e. ( F u. G ) z C_ ( w i^i y ) ) )
47 46 cbvralvw 
 |-  ( A. x e. F E. z e. ( F u. G ) z C_ ( x i^i y ) <-> A. w e. F E. z e. ( F u. G ) z C_ ( w i^i y ) )
48 47 ralbii 
 |-  ( A. y e. G A. x e. F E. z e. ( F u. G ) z C_ ( x i^i y ) <-> A. y e. G A. w e. F E. z e. ( F u. G ) z C_ ( w i^i y ) )
49 ineq2 
 |-  ( y = x -> ( w i^i y ) = ( w i^i x ) )
50 49 sseq2d 
 |-  ( y = x -> ( z C_ ( w i^i y ) <-> z C_ ( w i^i x ) ) )
51 50 rexbidv 
 |-  ( y = x -> ( E. z e. ( F u. G ) z C_ ( w i^i y ) <-> E. z e. ( F u. G ) z C_ ( w i^i x ) ) )
52 ineq1 
 |-  ( w = y -> ( w i^i x ) = ( y i^i x ) )
53 incom 
 |-  ( y i^i x ) = ( x i^i y )
54 52 53 eqtrdi 
 |-  ( w = y -> ( w i^i x ) = ( x i^i y ) )
55 54 sseq2d 
 |-  ( w = y -> ( z C_ ( w i^i x ) <-> z C_ ( x i^i y ) ) )
56 55 rexbidv 
 |-  ( w = y -> ( E. z e. ( F u. G ) z C_ ( w i^i x ) <-> E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
57 51 56 cbvral2vw 
 |-  ( A. y e. G A. w e. F E. z e. ( F u. G ) z C_ ( w i^i y ) <-> A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
58 43 48 57 3bitri 
 |-  ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) <-> A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
59 58 biimpi 
 |-  ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) )
60 ssun2 
 |-  G C_ ( F u. G )
61 fbasssin 
 |-  ( ( G e. ( fBas ` X ) /\ x e. G /\ y e. G ) -> E. z e. G z C_ ( x i^i y ) )
62 ssrexv 
 |-  ( G C_ ( F u. G ) -> ( E. z e. G z C_ ( x i^i y ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
63 60 61 62 mpsyl 
 |-  ( ( G e. ( fBas ` X ) /\ x e. G /\ y e. G ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
64 63 3expb 
 |-  ( ( G e. ( fBas ` X ) /\ ( x e. G /\ y e. G ) ) -> E. z e. ( F u. G ) z C_ ( x i^i y ) )
65 64 ralrimivva 
 |-  ( G e. ( fBas ` X ) -> A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) )
66 65 adantl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) )
67 59 66 anim12i 
 |-  ( ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) /\ ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) ) -> ( A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
68 67 expcom 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) )
69 r19.26 
 |-  ( A. x e. G ( A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) <-> ( A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
70 39 ralimi 
 |-  ( A. x e. G ( A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. x e. G A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
71 69 70 sylbir 
 |-  ( ( A. x e. G A. y e. F E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. x e. G A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
72 68 71 syl6 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> A. x e. G A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
73 42 72 jcad 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( A. x e. F A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) )
74 ralun 
 |-  ( ( A. x e. F A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) /\ A. x e. G A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) -> A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) )
75 73 74 syl6 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) )
76 19 29 75 3jcad 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( ( F u. G ) =/= (/) /\ (/) e/ ( F u. G ) /\ A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) )
77 13 76 jcad 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( ( F u. G ) C_ ~P X /\ ( ( F u. G ) =/= (/) /\ (/) e/ ( F u. G ) /\ A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) ) )
78 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
79 78 adantr 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> X e. dom fBas )
80 isfbas2 
 |-  ( X e. dom fBas -> ( ( F u. G ) e. ( fBas ` X ) <-> ( ( F u. G ) C_ ~P X /\ ( ( F u. G ) =/= (/) /\ (/) e/ ( F u. G ) /\ A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) ) )
81 79 80 syl 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( F u. G ) e. ( fBas ` X ) <-> ( ( F u. G ) C_ ~P X /\ ( ( F u. G ) =/= (/) /\ (/) e/ ( F u. G ) /\ A. x e. ( F u. G ) A. y e. ( F u. G ) E. z e. ( F u. G ) z C_ ( x i^i y ) ) ) ) )
82 77 81 sylibrd 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) -> ( F u. G ) e. ( fBas ` X ) ) )
83 7 82 impbid2 
 |-  ( ( F e. ( fBas ` X ) /\ G e. ( fBas ` X ) ) -> ( ( F u. G ) e. ( fBas ` X ) <-> A. x e. F A. y e. G E. z e. ( F u. G ) z C_ ( x i^i y ) ) )