Theorem cvnsym

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

	Ref	Expression
Assertion	cvnsym	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{⋖}_{\mathscr{H}}B\to \neg B{⋖}_{\mathscr{H}}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		cvpss	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{⋖}_{\mathscr{H}}B\to A\subset B\right)$$
2		cvpss	$$⊢\left(B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{⋖}_{\mathscr{H}}A\to B\subset A\right)$$
3	2	ancoms	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{⋖}_{\mathscr{H}}A\to B\subset A\right)$$
4		pssn2lp	$$⊢\neg \left(B\subset A\wedge A\subset B\right)$$
5	4	imnani	$$⊢B\subset A\to \neg A\subset B$$
6	3 5	syl6	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(B{⋖}_{\mathscr{H}}A\to \neg A\subset B\right)$$
7	6	con2d	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subset B\to \neg B{⋖}_{\mathscr{H}}A\right)$$
8	1 7	syld	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A{⋖}_{\mathscr{H}}B\to \neg B{⋖}_{\mathscr{H}}A\right)$$