# Metamath Proof Explorer

## Theorem meet0

Description: Lemma for odujoin . (Contributed by Stefan O'Rear, 29-Jan-2015) TODO ( df-riota update): This proof increased from 152 bytes to 547 bytes after the df-riota change. Any way to shorten it? join0 also.

Ref Expression
Assertion meet0 ${⊢}\mathrm{meet}\left(\varnothing \right)=\varnothing$

### Proof

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