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

Metamath Proof Explorer

Theorem meetcom

Description: The meet of a poset is commutative. (The antecedent <. X , Y >. e. dom ./\ /\ <. Y , X >. e. dom ./\ i.e., "the meets exist" could be omitted as an artifact of our particular join definition, but other definitions may require it.) (Contributed by NM, 17-Sep-2011) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	meetcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	meetcom	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		meetcom.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		meetcom.m	⊢ ∧ = ( meet ‘ 𝐾 )
3	1 2	meetcomALT	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
4	3	adantr	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ ∧ ⟨ 𝑌 , 𝑋 ⟩ ∈ dom ∧ ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )