Metamath Proof Explorer


Theorem cvrntr

Description: The covers relation is not transitive. ( cvntr analog.) (Contributed by NM, 18-Jun-2012)

Ref Expression
Hypotheses cvrntr.b 𝐵 = ( Base ‘ 𝐾 )
cvrntr.c 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrntr ( ( 𝐾𝐴 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 𝐶 𝑌𝑌 𝐶 𝑍 ) → ¬ 𝑋 𝐶 𝑍 ) )

Proof

Step Hyp Ref Expression
1 cvrntr.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrntr.c 𝐶 = ( ⋖ ‘ 𝐾 )
3 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
4 1 3 2 cvrlt ( ( ( 𝐾𝐴𝑋𝐵𝑌𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ( lt ‘ 𝐾 ) 𝑌 )
5 4 ex ( ( 𝐾𝐴𝑋𝐵𝑌𝐵 ) → ( 𝑋 𝐶 𝑌𝑋 ( lt ‘ 𝐾 ) 𝑌 ) )
6 5 3adant3r3 ( ( 𝐾𝐴 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( 𝑋 𝐶 𝑌𝑋 ( lt ‘ 𝐾 ) 𝑌 ) )
7 1 3 2 ltcvrntr ( ( 𝐾𝐴 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 ( lt ‘ 𝐾 ) 𝑌𝑌 𝐶 𝑍 ) → ¬ 𝑋 𝐶 𝑍 ) )
8 6 7 syland ( ( 𝐾𝐴 ∧ ( 𝑋𝐵𝑌𝐵𝑍𝐵 ) ) → ( ( 𝑋 𝐶 𝑌𝑌 𝐶 𝑍 ) → ¬ 𝑋 𝐶 𝑍 ) )