# 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 ${⊢}\left({F}\in \mathrm{fBas}\left({X}\right)\wedge {G}\in \mathrm{fBas}\left({X}\right)\right)\to \left({F}\cup {G}\in \mathrm{fBas}\left({X}\right)↔\forall {x}\in {F}\phantom{\rule{.4em}{0ex}}\forall {y}\in {G}\phantom{\rule{.4em}{0ex}}\exists {z}\in \left({F}\cup {G}\right)\phantom{\rule{.4em}{0ex}}{z}\subseteq {x}\cap {y}\right)$

### Proof

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