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 fBas X G fBas X F G fBas X x F y G z F G z x y

Proof

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