This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )