Theorem lemeet1

Description: A meet's first argument is less than or equal to the meet. (Contributed by NM, 16-Sep-2011) (Revised by NM, 12-Sep-2018)

	Ref	Expression
Hypotheses	meetval2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	meetval2.l	⊢ ≤ = ( le ‘ 𝐾 )
	meetval2.m	⊢ ∧ = ( meet ‘ 𝐾 )
	meetval2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	meetval2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	meetval2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	meetlem.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
Assertion	lemeet1	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		meetval2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		meetval2.l	⊢ ≤ = ( le ‘ 𝐾 )
3		meetval2.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		meetval2.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5		meetval2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		meetval2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		meetlem.e	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑌 ⟩ ∈ dom ∧ )
8	1 2 3 4 5 6 7	meetlem	⊢ ( 𝜑 → ( ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≤ 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑧 ≤ 𝑋 ∧ 𝑧 ≤ 𝑌 ) → 𝑧 ≤ ( 𝑋 ∧ 𝑌 ) ) ) )
9	8	simplld	⊢ ( 𝜑 → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )