Theorem cvnref

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

	Ref	Expression
Assertion	cvnref	⊢ ( 𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cvnsym	⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐴 → ¬ 𝐴 ⋖ℋ 𝐴 ) )
2	1	anidms	⊢ ( 𝐴 ∈ Cℋ → ( 𝐴 ⋖ℋ 𝐴 → ¬ 𝐴 ⋖ℋ 𝐴 ) )
3	2	pm2.01d	⊢ ( 𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴 )