Description: The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | cvnsym | ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴 ) ) |
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ℋ ) → ( 𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴 ) ) |