Theorem latmlej21

Description: Ordering of a meet and join with a common variable. (Contributed by NM, 4-Oct-2012)

	Ref	Expression
Hypotheses	latledi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latledi.l	⊢ ≤ = ( le ‘ 𝐾 )
	latledi.j	⊢ ∨ = ( join ‘ 𝐾 )
	latledi.m	⊢ ∧ = ( meet ‘ 𝐾 )
Assertion	latmlej21	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∧ 𝑋 ) ≤ ( 𝑋 ∨ 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		latledi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latledi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latledi.j	⊢ ∨ = ( join ‘ 𝐾 )
4		latledi.m	⊢ ∧ = ( meet ‘ 𝐾 )
5	1 4	latmcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
6	5	3adant3r3	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) = ( 𝑌 ∧ 𝑋 ) )
7	1 2 3 4	latmlej11	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑋 ∨ 𝑍 ) )
8	6 7	eqbrtrrd	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ∧ 𝑋 ) ≤ ( 𝑋 ∨ 𝑍 ) )