Metamath Proof Explorer


Theorem joinfval2

Description: Value of join function for a poset-type structure. (Contributed by NM, 12-Sep-2011) (Revised by NM, 9-Sep-2018)

Ref Expression
Hypotheses joinfval.u U=lubK
joinfval.j ˙=joinK
Assertion joinfval2 KV˙=xyz|xydomUz=Uxy

Proof

Step Hyp Ref Expression
1 joinfval.u U=lubK
2 joinfval.j ˙=joinK
3 1 2 joinfval KV˙=xyz|xyUz
4 1 lubfun FunU
5 funbrfv2b FunUxyUzxydomUUxy=z
6 4 5 ax-mp xyUzxydomUUxy=z
7 eqcom Uxy=zz=Uxy
8 7 anbi2i xydomUUxy=zxydomUz=Uxy
9 6 8 bitri xyUzxydomUz=Uxy
10 9 oprabbii xyz|xyUz=xyz|xydomUz=Uxy
11 3 10 eqtrdi KV˙=xyz|xydomUz=Uxy