Metamath Proof Explorer

Theorem ltltncvr

Description: A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses ltltncvr.b ⊢ B = Base K
ltltncvr.s ⊢ < ˙ = < K
ltltncvr.c ⊢ C = ⋖ K
Assertion ltltncvr ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X < ˙ Y ∧ Y < ˙ Z → ¬ X C Z

Proof

Step Hyp Ref Expression
1 ltltncvr.b ⊢ B = Base K
2 ltltncvr.s ⊢ < ˙ = < K
3 ltltncvr.c ⊢ C = ⋖ K
4 simpll ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → K ∈ A
5 simplr1 ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → X ∈ B
6 simplr3 ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → Z ∈ B
7 simplr2 ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → Y ∈ B
8 simpr ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → X C Z
9 1 2 3 cvrnbtwn ⊢ K ∈ A ∧ X ∈ B ∧ Z ∈ B ∧ Y ∈ B ∧ X C Z → ¬ X < ˙ Y ∧ Y < ˙ Z
10 4 5 6 7 8 9 syl131anc ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B ∧ X C Z → ¬ X < ˙ Y ∧ Y < ˙ Z
11 10 ex ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X C Z → ¬ X < ˙ Y ∧ Y < ˙ Z
12 11 con2d ⊢ K ∈ A ∧ X ∈ B ∧ Y ∈ B ∧ Z ∈ B → X < ˙ Y ∧ Y < ˙ Z → ¬ X C Z