Metamath Proof Explorer


Theorem joindef

Description: Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018)

Ref Expression
Hypotheses joindef.u U=lubK
joindef.j ˙=joinK
joindef.k φKV
joindef.x φXW
joindef.y φYZ
Assertion joindef φXYdom˙XYdomU

Proof

Step Hyp Ref Expression
1 joindef.u U=lubK
2 joindef.j ˙=joinK
3 joindef.k φKV
4 joindef.x φXW
5 joindef.y φYZ
6 1 2 joindm KVdom˙=xy|xydomU
7 6 eleq2d KVXYdom˙XYxy|xydomU
8 3 7 syl φXYdom˙XYxy|xydomU
9 preq1 x=Xxy=Xy
10 9 eleq1d x=XxydomUXydomU
11 preq2 y=YXy=XY
12 11 eleq1d y=YXydomUXYdomU
13 10 12 opelopabg XWYZXYxy|xydomUXYdomU
14 4 5 13 syl2anc φXYxy|xydomUXYdomU
15 8 14 bitrd φXYdom˙XYdomU