Theorem latnle

Description: Equivalent expressions for "not less than" in a lattice. ( chnle analog.) (Contributed by NM, 16-Nov-2011)

	Ref	Expression
Hypotheses	latnle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	latnle.l	⊢ ≤ = ( le ‘ 𝐾 )
	latnle.s	⊢ < = ( lt ‘ 𝐾 )
	latnle.j	⊢ ∨ = ( join ‘ 𝐾 )
Assertion	latnle	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < ( 𝑋 ∨ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		latnle.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latnle.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latnle.s	⊢ < = ( lt ‘ 𝐾 )
4		latnle.j	⊢ ∨ = ( join ‘ 𝐾 )
5	1 2 4	latlej1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) )
6	5	biantrurd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≠ ( 𝑋 ∨ 𝑌 ) ↔ ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑋 ≠ ( 𝑋 ∨ 𝑌 ) ) ) )
7	1 2 4	latleeqj1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ( 𝑌 ∨ 𝑋 ) = 𝑋 ) )
8	7	3com23	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ ( 𝑌 ∨ 𝑋 ) = 𝑋 ) )
9		eqcom	⊢ ( ( 𝑌 ∨ 𝑋 ) = 𝑋 ↔ 𝑋 = ( 𝑌 ∨ 𝑋 ) )
10	8 9	bitrdi	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ 𝑋 = ( 𝑌 ∨ 𝑋 ) ) )
11	1 4	latjcom	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) = ( 𝑌 ∨ 𝑋 ) )
12	11	eqeq2d	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = ( 𝑋 ∨ 𝑌 ) ↔ 𝑋 = ( 𝑌 ∨ 𝑋 ) ) )
13	10 12	bitr4d	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ 𝑋 = ( 𝑋 ∨ 𝑌 ) ) )
14	13	necon3bbid	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ 𝑋 ≠ ( 𝑋 ∨ 𝑌 ) ) )
15	1 4	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
16	2 3	pltval	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ) → ( 𝑋 < ( 𝑋 ∨ 𝑌 ) ↔ ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑋 ≠ ( 𝑋 ∨ 𝑌 ) ) ) )
17	15 16	syld3an3	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < ( 𝑋 ∨ 𝑌 ) ↔ ( 𝑋 ≤ ( 𝑋 ∨ 𝑌 ) ∧ 𝑋 ≠ ( 𝑋 ∨ 𝑌 ) ) ) )
18	6 14 17	3bitr4d	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑌 ≤ 𝑋 ↔ 𝑋 < ( 𝑋 ∨ 𝑌 ) ) )