Theorem latnlemlt

Description: Negation of "less than or equal to" expressed in terms of meet and less-than. ( nssinpss analog.) (Contributed by NM, 5-Feb-2012)

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

Proof

Step	Hyp	Ref	Expression
1		latnlemlt.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		latnlemlt.l	⊢ ≤ = ( le ‘ 𝐾 )
3		latnlemlt.s	⊢ < = ( lt ‘ 𝐾 )
4		latnlemlt.m	⊢ ∧ = ( meet ‘ 𝐾 )
5	1 2 4	latmle1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 )
6	5	biantrurd	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ↔ ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) ) )
7	1 2 4	latleeqm1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) = 𝑋 ) )
8	7	necon3bbid	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) )
9		simp1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Lat )
10	1 4	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
11		simp2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
12	2 3	pltval	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) < 𝑋 ↔ ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) ) )
13	9 10 11 12	syl3anc	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) < 𝑋 ↔ ( ( 𝑋 ∧ 𝑌 ) ≤ 𝑋 ∧ ( 𝑋 ∧ 𝑌 ) ≠ 𝑋 ) ) )
14	6 8 13	3bitr4d	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ¬ 𝑋 ≤ 𝑌 ↔ ( 𝑋 ∧ 𝑌 ) < 𝑋 ) )