Theorem chsscon3

Description: Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	chsscon3	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq B\leftrightarrow \perp \left(B\right)\subseteq \perp \left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(A\subseteq B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq B\right)$$
2		fveq2	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \perp \left(A\right)=\perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
3	2	sseq2d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\perp \left(B\right)\subseteq \perp \left(A\right)\leftrightarrow \perp \left(B\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\right)$$
4	1 3	bibi12d	$$⊢A=if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\to \left(\left(A\subseteq B\leftrightarrow \perp \left(B\right)\subseteq \perp \left(A\right)\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq B\leftrightarrow \perp \left(B\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\right)\right)$$
5		sseq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq B\leftrightarrow if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
6		fveq2	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \perp \left(B\right)=\perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)$$
7	6	sseq1d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\perp \left(B\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\leftrightarrow \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\right)$$
8	5 7	bibi12d	$$⊢B=if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\to \left(\left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq B\leftrightarrow \perp \left(B\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\right)\leftrightarrow \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\leftrightarrow \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)\right)\right)$$
9		ifchhv	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
10		ifchhv	$$⊢if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\in {\mathbf{C}}_{\mathscr{H}}$$
11	9 10	chsscon3i	$$⊢if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\subseteq if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\leftrightarrow \perp \left(if\left(B\in {\mathbf{C}}_{\mathscr{H}},B,\mathscr{H}\right)\right)\subseteq \perp \left(if\left(A\in {\mathbf{C}}_{\mathscr{H}},A,\mathscr{H}\right)\right)$$
12	4 8 11	dedth2h	$$⊢\left(A\in {\mathbf{C}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\right)\to \left(A\subseteq B\leftrightarrow \perp \left(B\right)\subseteq \perp \left(A\right)\right)$$