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

Metamath Proof Explorer

Theorem pleval2i

Description: One direction of pleval2 . (Contributed by Mario Carneiro, 8-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 pleval2.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 pleval2.l ⊢ ≤ = ( le ‘ 𝐾 )
3 pleval2.s ⊢ < = ( lt ‘ 𝐾 )
4 elfvdm ⊢ ( 𝑋 ∈ ( Base ‘ 𝐾 ) → 𝐾 ∈ dom Base )
5 4 1 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → 𝐾 ∈ dom Base )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ dom Base )
7 2 3 pltval ⊢ ( ( 𝐾 ∈ dom Base ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
8 7 3expb ⊢ ( ( 𝐾 ∈ dom Base ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
9 6 8 mpancom ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 < 𝑌 ↔ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) )
10 9 biimpar ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ≤ 𝑌 ∧ 𝑋 ≠ 𝑌 ) ) → 𝑋 < 𝑌 )
11 10 expr ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 ≠ 𝑌 → 𝑋 < 𝑌 ) )
12 11 necon1bd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( ¬ 𝑋 < 𝑌 → 𝑋 = 𝑌 ) )
13 12 orrd ⊢ ( ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) )
14 13 ex ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 → ( 𝑋 < 𝑌 ∨ 𝑋 = 𝑌 ) ) )