# Metamath Proof Explorer

## 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}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}↔\perp \left({B}\right)\subseteq \perp \left({A}\right)\right)$

### Proof

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