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

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 ⊢ ( ( 𝐾 ∈ 𝐴 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑌 ∧ 𝑌 𝐶 𝑍 ) → ¬ 𝑋 𝐶 𝑍 ) )