# Metamath Proof Explorer

## Theorem join0

Description: Lemma for odumeet . (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Assertion join0 ${⊢}\mathrm{join}\left(\varnothing \right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 eqid ${⊢}\mathrm{lub}\left(\varnothing \right)=\mathrm{lub}\left(\varnothing \right)$
3 eqid ${⊢}\mathrm{join}\left(\varnothing \right)=\mathrm{join}\left(\varnothing \right)$
4 2 3 joinfval ${⊢}\varnothing \in \mathrm{V}\to \mathrm{join}\left(\varnothing \right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right\}$
5 1 4 ax-mp ${⊢}\mathrm{join}\left(\varnothing \right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right\}$
6 df-oprab ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)\right\}$
7 br0 ${⊢}¬\left\{{x},{y}\right\}\varnothing {z}$
8 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
9 eqid ${⊢}{\le }_{\varnothing }={\le }_{\varnothing }$
10 biid ${⊢}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)↔\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)$
11 id ${⊢}\varnothing \in \mathrm{V}\to \varnothing \in \mathrm{V}$
12 8 9 2 10 11 lubfval ${⊢}\varnothing \in \mathrm{V}\to \mathrm{lub}\left(\varnothing \right)={\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\left\{{w}|\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right\}}$
13 1 12 ax-mp ${⊢}\mathrm{lub}\left(\varnothing \right)={\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\left\{{w}|\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right\}}$
14 reu0 ${⊢}¬\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)$
15 14 abf ${⊢}\left\{{w}|\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right\}=\varnothing$
16 15 reseq2i ${⊢}{\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\left\{{w}|\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right\}}={\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\varnothing }$
17 res0 ${⊢}{\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\varnothing }=\varnothing$
18 16 17 eqtri ${⊢}{\left({w}\in 𝒫\varnothing ⟼\left(\iota {z}\in \varnothing |\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right)\right)↾}_{\left\{{w}|\exists !{z}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{z}\wedge \forall {y}\in \varnothing \phantom{\rule{.4em}{0ex}}\left(\forall {x}\in {w}\phantom{\rule{.4em}{0ex}}{x}{\le }_{\varnothing }{y}\to {z}{\le }_{\varnothing }{y}\right)\right)\right\}}=\varnothing$
19 13 18 eqtri ${⊢}\mathrm{lub}\left(\varnothing \right)=\varnothing$
20 19 breqi ${⊢}\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}↔\left\{{x},{y}\right\}\varnothing {z}$
21 7 20 mtbir ${⊢}¬\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}$
22 21 intnan ${⊢}¬\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)$
23 22 nex ${⊢}¬\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)$
24 23 nex ${⊢}¬\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)$
25 24 nex ${⊢}¬\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)$
26 25 abf ${⊢}\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge \left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right)\right\}=\varnothing$
27 6 26 eqtri ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left(\varnothing \right){z}\right\}=\varnothing$
28 5 27 eqtri ${⊢}\mathrm{join}\left(\varnothing \right)=\varnothing$