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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	joincom.j	⊢ ∨ = ( join ‘ 𝐾 )
Assertion	joincomALT	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		joincom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		joincom.j	⊢ ∨ = ( join ‘ 𝐾 )
3		prcom	⊢ { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
4	3	fveq2i	⊢ ( ( lub ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } )
5	4	a1i	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( lub ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
6		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
7		simp1	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ 𝑉 )
8		simp3	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
9		simp2	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10	6 2 7 8 9	joinval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∨ 𝑋 ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) )
11	6 2 7 9 8	joinval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( ( lub ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
12	5 10 11	3eqtr4rd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )