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

Metamath Proof Explorer

Theorem cvrlt

Description: The covers relation implies the less-than relation. ( cvpss analog.) (Contributed by NM, 8-Oct-2011)

Ref Expression
Hypotheses cvrfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrfval.s ⊢ < = ( lt ‘ 𝐾 )
cvrfval.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrlt ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )

Proof

Step Hyp Ref Expression
1 cvrfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrfval.s ⊢ < = ( lt ‘ 𝐾 )
3 cvrfval.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 1 2 3 cvrval ⊢ ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( 𝑋 < 𝑌 ∧ ¬ ∃ 𝑧 ∈ 𝐵 ( 𝑋 < 𝑧 ∧ 𝑧 < 𝑌 ) ) ) )
5 4 simprbda ⊢ ( ( ( 𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )