# Metamath Proof Explorer

## Theorem joinfval

Description: Value of join function for a poset. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018) TODO: prove joinfval2 first to reduce net proof size (existence part)?

Ref Expression
Hypotheses joinfval.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
joinfval.j
Assertion joinfval

### Proof

Step Hyp Ref Expression
1 joinfval.u ${⊢}{U}=\mathrm{lub}\left({K}\right)$
2 joinfval.j
3 elex ${⊢}{K}\in {V}\to {K}\in \mathrm{V}$
4 fvex ${⊢}{\mathrm{Base}}_{{K}}\in \mathrm{V}$
5 moeq ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{z}={U}\left(\left\{{x},{y}\right\}\right)$
6 5 a1i ${⊢}\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\to {\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{z}={U}\left(\left\{{x},{y}\right\}\right)$
7 eqid ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}$
8 4 4 6 7 oprabex ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}\in \mathrm{V}$
9 8 a1i ${⊢}{K}\in \mathrm{V}\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}\in \mathrm{V}$
10 1 lubfun ${⊢}\mathrm{Fun}{U}$
11 funbrfv2b ${⊢}\mathrm{Fun}{U}\to \left(\left\{{x},{y}\right\}{U}{z}↔\left(\left\{{x},{y}\right\}\in \mathrm{dom}{U}\wedge {U}\left(\left\{{x},{y}\right\}\right)={z}\right)\right)$
12 10 11 ax-mp ${⊢}\left\{{x},{y}\right\}{U}{z}↔\left(\left\{{x},{y}\right\}\in \mathrm{dom}{U}\wedge {U}\left(\left\{{x},{y}\right\}\right)={z}\right)$
13 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
14 eqid ${⊢}{\le }_{{K}}={\le }_{{K}}$
15 simpl ${⊢}\left({K}\in \mathrm{V}\wedge \left\{{x},{y}\right\}\in \mathrm{dom}{U}\right)\to {K}\in \mathrm{V}$
16 simpr ${⊢}\left({K}\in \mathrm{V}\wedge \left\{{x},{y}\right\}\in \mathrm{dom}{U}\right)\to \left\{{x},{y}\right\}\in \mathrm{dom}{U}$
17 13 14 1 15 16 lubelss ${⊢}\left({K}\in \mathrm{V}\wedge \left\{{x},{y}\right\}\in \mathrm{dom}{U}\right)\to \left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{K}}$
18 17 ex ${⊢}{K}\in \mathrm{V}\to \left(\left\{{x},{y}\right\}\in \mathrm{dom}{U}\to \left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{K}}\right)$
19 vex ${⊢}{x}\in \mathrm{V}$
20 vex ${⊢}{y}\in \mathrm{V}$
21 19 20 prss ${⊢}\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)↔\left\{{x},{y}\right\}\subseteq {\mathrm{Base}}_{{K}}$
22 18 21 syl6ibr ${⊢}{K}\in \mathrm{V}\to \left(\left\{{x},{y}\right\}\in \mathrm{dom}{U}\to \left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\right)$
23 eqcom ${⊢}{U}\left(\left\{{x},{y}\right\}\right)={z}↔{z}={U}\left(\left\{{x},{y}\right\}\right)$
24 23 biimpi ${⊢}{U}\left(\left\{{x},{y}\right\}\right)={z}\to {z}={U}\left(\left\{{x},{y}\right\}\right)$
25 22 24 anim12d1 ${⊢}{K}\in \mathrm{V}\to \left(\left(\left\{{x},{y}\right\}\in \mathrm{dom}{U}\wedge {U}\left(\left\{{x},{y}\right\}\right)={z}\right)\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)$
26 12 25 syl5bi ${⊢}{K}\in \mathrm{V}\to \left(\left\{{x},{y}\right\}{U}{z}\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)$
27 26 alrimiv ${⊢}{K}\in \mathrm{V}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}{U}{z}\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)$
28 27 alrimiv ${⊢}{K}\in \mathrm{V}\to \forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}{U}{z}\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)$
29 28 alrimiv ${⊢}{K}\in \mathrm{V}\to \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}{U}{z}\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)$
30 ssoprab2 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left\{{x},{y}\right\}{U}{z}\to \left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right)\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}\subseteq \left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}$
31 29 30 syl ${⊢}{K}\in \mathrm{V}\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}\subseteq \left\{⟨⟨{x},{y}⟩,{z}⟩|\left(\left({x}\in {\mathrm{Base}}_{{K}}\wedge {y}\in {\mathrm{Base}}_{{K}}\right)\wedge {z}={U}\left(\left\{{x},{y}\right\}\right)\right)\right\}$
32 9 31 ssexd ${⊢}{K}\in \mathrm{V}\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}\in \mathrm{V}$
33 fveq2 ${⊢}{p}={K}\to \mathrm{lub}\left({p}\right)=\mathrm{lub}\left({K}\right)$
34 33 1 eqtr4di ${⊢}{p}={K}\to \mathrm{lub}\left({p}\right)={U}$
35 34 breqd ${⊢}{p}={K}\to \left(\left\{{x},{y}\right\}\mathrm{lub}\left({p}\right){z}↔\left\{{x},{y}\right\}{U}{z}\right)$
36 35 oprabbidv ${⊢}{p}={K}\to \left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left({p}\right){z}\right\}=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}$
37 df-join ${⊢}\mathrm{join}=\left({p}\in \mathrm{V}⟼\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}\mathrm{lub}\left({p}\right){z}\right\}\right)$
38 36 37 fvmptg ${⊢}\left({K}\in \mathrm{V}\wedge \left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}\in \mathrm{V}\right)\to \mathrm{join}\left({K}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}$
39 32 38 mpdan ${⊢}{K}\in \mathrm{V}\to \mathrm{join}\left({K}\right)=\left\{⟨⟨{x},{y}⟩,{z}⟩|\left\{{x},{y}\right\}{U}{z}\right\}$
40 2 39 syl5eq
41 3 40 syl