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

Metamath Proof Explorer

Theorem pltval3

Description: Alternate expression for the "less than" relation. ( dfpss3 analog.) (Contributed by NM, 4-Nov-2011)

Ref Expression
Hypotheses pleval2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
pleval2.l ⊢ ≤ = ( le ‘ 𝐾 )
pleval2.s ⊢ < = ( lt ‘ 𝐾 )
Assertion pltval3 ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 pleval2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pleval2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pleval2.s ⊢ < = ( lt ‘ 𝐾 )
4 2 3 pltval ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
5 1 2 posref ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
6 5 3adant3 ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
7 breq1 ⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑌 ≤ 𝑋 ) )
8 6 7 syl5ibcom ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → 𝑌 ≤ 𝑋 ) )
9 8 adantr ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 = 𝑌 → 𝑌 ≤ 𝑋 ) )
10 1 2 posasymb ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )
11 10 biimpd ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) )
12 11 expdimp ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑌 ≤ 𝑋 → 𝑋 = 𝑌 ) )
13 9 12 impbid ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 = 𝑌 ↔ 𝑌 ≤ 𝑋 ) )
14 13 necon3abid ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ≠ 𝑌 ↔ ¬ 𝑌 ≤ 𝑋 ) )
15 14 pm5.32da ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ) )
16 4 15 bitrd ⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ ¬ 𝑌 ≤ 𝑋 ) ) )