# Metamath Proof Explorer

## Theorem meetval

Description: Meet value. Since both sides evaluate to (/) when they don't exist, for convenience we drop the { X , Y } e. dom G requirement. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypotheses meetdef.u ${⊢}{G}=\mathrm{glb}\left({K}\right)$
meetdef.m
meetdef.k ${⊢}{\phi }\to {K}\in {V}$
meetdef.x ${⊢}{\phi }\to {X}\in {W}$
meetdef.y ${⊢}{\phi }\to {Y}\in {Z}$
Assertion meetval

### Proof

Step Hyp Ref Expression
1 meetdef.u ${⊢}{G}=\mathrm{glb}\left({K}\right)$
2 meetdef.m
3 meetdef.k ${⊢}{\phi }\to {K}\in {V}$
4 meetdef.x ${⊢}{\phi }\to {X}\in {W}$
5 meetdef.y ${⊢}{\phi }\to {Y}\in {Z}$
6 1 2 meetfval2
7 3 6 syl
8 7 oveqd
10 simpr ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)\to \left\{{X},{Y}\right\}\in \mathrm{dom}{G}$
11 eqidd ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)\to {G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)$
12 fvexd ${⊢}{\phi }\to {G}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{V}$
13 preq12 ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to \left\{{x},{y}\right\}=\left\{{X},{Y}\right\}$
14 13 eleq1d ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to \left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}↔\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)$
15 14 3adant3 ${⊢}\left({x}={X}\wedge {y}={Y}\wedge {z}={G}\left(\left\{{X},{Y}\right\}\right)\right)\to \left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}↔\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)$
16 simp3 ${⊢}\left({x}={X}\wedge {y}={Y}\wedge {z}={G}\left(\left\{{X},{Y}\right\}\right)\right)\to {z}={G}\left(\left\{{X},{Y}\right\}\right)$
17 13 fveq2d ${⊢}\left({x}={X}\wedge {y}={Y}\right)\to {G}\left(\left\{{x},{y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)$
18 17 3adant3 ${⊢}\left({x}={X}\wedge {y}={Y}\wedge {z}={G}\left(\left\{{X},{Y}\right\}\right)\right)\to {G}\left(\left\{{x},{y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)$
19 16 18 eqeq12d ${⊢}\left({x}={X}\wedge {y}={Y}\wedge {z}={G}\left(\left\{{X},{Y}\right\}\right)\right)\to \left({z}={G}\left(\left\{{x},{y}\right\}\right)↔{G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)\right)$
20 15 19 anbi12d ${⊢}\left({x}={X}\wedge {y}={Y}\wedge {z}={G}\left(\left\{{X},{Y}\right\}\right)\right)\to \left(\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)↔\left(\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\wedge {G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)\right)\right)$
21 moeq ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{z}={G}\left(\left\{{x},{y}\right\}\right)$
22 21 moani ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)$
23 eqid ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}$
24 20 22 23 ovigg ${⊢}\left({X}\in {W}\wedge {Y}\in {Z}\wedge {G}\left(\left\{{X},{Y}\right\}\right)\in \mathrm{V}\right)\to \left(\left(\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\wedge {G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)\right)\to {X}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}{Y}={G}\left(\left\{{X},{Y}\right\}\right)\right)$
25 4 5 12 24 syl3anc ${⊢}{\phi }\to \left(\left(\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\wedge {G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)\right)\to {X}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}{Y}={G}\left(\left\{{X},{Y}\right\}\right)\right)$
26 25 adantr ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)\to \left(\left(\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\wedge {G}\left(\left\{{X},{Y}\right\}\right)={G}\left(\left\{{X},{Y}\right\}\right)\right)\to {X}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}{Y}={G}\left(\left\{{X},{Y}\right\}\right)\right)$
27 10 11 26 mp2and ${⊢}\left({\phi }\wedge \left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)\to {X}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left\{{x},{y}\right\}\in \mathrm{dom}{G}\wedge {z}={G}\left(\left\{{x},{y}\right\}\right)\right)\right\}{Y}={G}\left(\left\{{X},{Y}\right\}\right)$
28 9 27 eqtrd
29 1 2 3 4 5 meetdef
30 29 notbid
31 df-ov
32 ndmfv
33 31 32 syl5eq
34 30 33 syl6bir
35 34 imp
36 ndmfv ${⊢}¬\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\to {G}\left(\left\{{X},{Y}\right\}\right)=\varnothing$
37 36 adantl ${⊢}\left({\phi }\wedge ¬\left\{{X},{Y}\right\}\in \mathrm{dom}{G}\right)\to {G}\left(\left\{{X},{Y}\right\}\right)=\varnothing$
38 35 37 eqtr4d
39 28 38 pm2.61dan