Theorem pltval

Description: Less-than relation. ( df-pss analog.) (Contributed by NM, 12-Oct-2011)

	Ref	Expression
Hypotheses	pltval.l	⊢ ≤ = ( le ‘ 𝐾 )
	pltval.s	⊢ < = ( lt ‘ 𝐾 )
Assertion	pltval	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pltval.l	⊢ ≤ = ( le ‘ 𝐾 )
2		pltval.s	⊢ < = ( lt ‘ 𝐾 )
3	1 2	pltfval	⊢ ( 𝐾 ∈ 𝐴 → < = ( ≤ ∖ I ) )
4	3	breqd	⊢ ( 𝐾 ∈ 𝐴 → ( 𝑋 < 𝑌 ↔ 𝑋 ( ≤ ∖ I ) 𝑌 ) )
5		brdif	⊢ ( 𝑋 ( ≤ ∖ I ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌 ) )
6		ideqg	⊢ ( 𝑌 ∈ 𝐶 → ( 𝑋 I 𝑌 ↔ 𝑋 = 𝑌 ) )
7	6	necon3bbid	⊢ ( 𝑌 ∈ 𝐶 → ( ¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌 ) )
8	7	adantl	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( ¬ 𝑋 I 𝑌 ↔ 𝑋 ≠ 𝑌 ) )
9	8	anbi2d	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑋 I 𝑌 ) ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
10	5 9	syl5bb	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 ( ≤ ∖ I ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
11	4 10	sylan9bb	⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
12	11	3impb	⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )