This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 ( ≤ ∖ I ) 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
11 4 10 sylan9bb ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
12 11 3impb ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐶 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )