Theorem meetcomALT

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

	Ref	Expression
Hypotheses	meetcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	meetcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	meetcomALT	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		meetcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		meetcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
3		prcom	⊢ { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
4	3	fveq2i	⊢ ( ( glb ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } )
5	4	a1i	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
6		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
7		simp1	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ 𝑉 )
8		simp3	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
9		simp2	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
10	6 2 7 8 9	meetval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∧ 𝑋 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑌 , 𝑋 } ) )
11	6 2 7 9 8	meetval	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( ( glb ‘ 𝐾 ) ‘ { 𝑋 , 𝑌 } ) )
12	5 10 11	3eqtr4rd	⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )