Theorem latmlej12

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	latmlej12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ∧ 𝑌 ) ≤ ( 𝑍 ∨ 𝑋 ) )

Proof

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