Metamath Proof Explorer


Theorem cvnsym

Description: The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvnsym ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 → ¬ 𝐵 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cvpss ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵𝐴𝐵 ) )
2 cvpss ( ( 𝐵C𝐴C ) → ( 𝐵 𝐴𝐵𝐴 ) )
3 2 ancoms ( ( 𝐴C𝐵C ) → ( 𝐵 𝐴𝐵𝐴 ) )
4 pssn2lp ¬ ( 𝐵𝐴𝐴𝐵 )
5 4 imnani ( 𝐵𝐴 → ¬ 𝐴𝐵 )
6 3 5 syl6 ( ( 𝐴C𝐵C ) → ( 𝐵 𝐴 → ¬ 𝐴𝐵 ) )
7 6 con2d ( ( 𝐴C𝐵C ) → ( 𝐴𝐵 → ¬ 𝐵 𝐴 ) )
8 1 7 syld ( ( 𝐴C𝐵C ) → ( 𝐴 𝐵 → ¬ 𝐵 𝐴 ) )