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∪Gz⊆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∪Gz⊆x∩y
5 4 3expb ⊢F∪G∈fBas⁡X∧x∈F∪G∧y∈F∪G→∃z∈F∪Gz⊆x∩y
6 3 5 sylan2 ⊢F∪G∈fBas⁡X∧x∈F∧y∈G→∃z∈F∪Gz⊆x∩y
7 6 ralrimivva ⊢F∪G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆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∪Gz⊆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∪Gz⊆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∪Gz⊆x∩y→∅∉F∪G
30 fbasssin ⊢F∈fBas⁡X∧x∈F∧y∈F→∃z∈Fz⊆x∩y
31 ssrexv ⊢F⊆F∪G→∃z∈Fz⊆x∩y→∃z∈F∪Gz⊆x∩y
32 14 30 31 mpsyl ⊢F∈fBas⁡X∧x∈F∧y∈F→∃z∈F∪Gz⊆x∩y
33 32 3expb ⊢F∈fBas⁡X∧x∈F∧y∈F→∃z∈F∪Gz⊆x∩y
34 33 ralrimivva ⊢F∈fBas⁡X→∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y
35 34 adantr ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y
36 pm3.2 ⊢∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y
37 35 36 syl ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y
38 r19.26 ⊢∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀y∈G∃z∈F∪Gz⊆x∩y↔∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y
39 ralun ⊢∀y∈F∃z∈F∪Gz⊆x∩y∧∀y∈G∃z∈F∪Gz⊆x∩y→∀y∈F∪G∃z∈F∪Gz⊆x∩y
40 39 ralimi ⊢∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∪G∃z∈F∪Gz⊆x∩y
41 38 40 sylbir ⊢∀x∈F∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∪G∃z∈F∪Gz⊆x∩y
42 37 41 syl6 ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∪G∃z∈F∪Gz⊆x∩y
43 ralcom ⊢∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y↔∀y∈G∀x∈F∃z∈F∪Gz⊆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∪Gz⊆x∩y↔∃z∈F∪Gz⊆w∩y
47 46 cbvralvw ⊢∀x∈F∃z∈F∪Gz⊆x∩y↔∀w∈F∃z∈F∪Gz⊆w∩y
48 47 ralbii ⊢∀y∈G∀x∈F∃z∈F∪Gz⊆x∩y↔∀y∈G∀w∈F∃z∈F∪Gz⊆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∪Gz⊆w∩y↔∃z∈F∪Gz⊆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∪Gz⊆w∩x↔∃z∈F∪Gz⊆x∩y
57 51 56 cbvral2vw ⊢∀y∈G∀w∈F∃z∈F∪Gz⊆w∩y↔∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y
58 43 48 57 3bitri ⊢∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y↔∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y
59 58 biimpi ⊢∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y
60 ssun2 ⊢G⊆F∪G
61 fbasssin ⊢G∈fBas⁡X∧x∈G∧y∈G→∃z∈Gz⊆x∩y
62 ssrexv ⊢G⊆F∪G→∃z∈Gz⊆x∩y→∃z∈F∪Gz⊆x∩y
63 60 61 62 mpsyl ⊢G∈fBas⁡X∧x∈G∧y∈G→∃z∈F∪Gz⊆x∩y
64 63 3expb ⊢G∈fBas⁡X∧x∈G∧y∈G→∃z∈F∪Gz⊆x∩y
65 64 ralrimivva ⊢G∈fBas⁡X→∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y
66 65 adantl ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y
67 59 66 anim12i ⊢∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y∧F∈fBas⁡X∧G∈fBas⁡X→∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y
68 67 expcom ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y
69 r19.26 ⊢∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀y∈G∃z∈F∪Gz⊆x∩y↔∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y
70 39 ralimi ⊢∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈G∀y∈F∪G∃z∈F∪Gz⊆x∩y
71 69 70 sylbir ⊢∀x∈G∀y∈F∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈G∀y∈F∪G∃z∈F∪Gz⊆x∩y
72 68 71 syl6 ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈G∀y∈F∪G∃z∈F∪Gz⊆x∩y
73 42 72 jcad ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∀y∈F∪G∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈F∪G∃z∈F∪Gz⊆x∩y
74 ralun ⊢∀x∈F∀y∈F∪G∃z∈F∪Gz⊆x∩y∧∀x∈G∀y∈F∪G∃z∈F∪Gz⊆x∩y→∀x∈F∪G∀y∈F∪G∃z∈F∪Gz⊆x∩y
75 73 74 syl6 ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→∀x∈F∪G∀y∈F∪G∃z∈F∪Gz⊆x∩y
76 19 29 75 3jcad ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→F∪G≠∅∧∅∉F∪G∧∀x∈F∪G∀y∈F∪G∃z∈F∪Gz⊆x∩y
77 13 76 jcad ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆x∩y→F∪G⊆𝒫X∧F∪G≠∅∧∅∉F∪G∧∀x∈F∪G∀y∈F∪G∃z∈F∪Gz⊆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∪Gz⊆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∪Gz⊆x∩y
82 77 81 sylibrd ⊢F∈fBas⁡X∧G∈fBas⁡X→∀x∈F∀y∈G∃z∈F∪Gz⊆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∪Gz⊆x∩y