Metamath Proof Explorer


Theorem joincomALT

Description: The join of a poset is commutative. (This may not be a theorem under other definitions of meet.) (Contributed by NM, 16-Sep-2011) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses joincom.b B=BaseK
joincom.j ˙=joinK
Assertion joincomALT KVXBYBX˙Y=Y˙X

Proof

Step Hyp Ref Expression
1 joincom.b B=BaseK
2 joincom.j ˙=joinK
3 prcom YX=XY
4 3 fveq2i lubKYX=lubKXY
5 4 a1i KVXBYBlubKYX=lubKXY
6 eqid lubK=lubK
7 simp1 KVXBYBKV
8 simp3 KVXBYBYB
9 simp2 KVXBYBXB
10 6 2 7 8 9 joinval KVXBYBY˙X=lubKYX
11 6 2 7 9 8 joinval KVXBYBX˙Y=lubKXY
12 5 10 11 3eqtr4rd KVXBYBX˙Y=Y˙X