Metamath Proof Explorer

Theorem chcon3i

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

Ref Expression
Hypotheses ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
Assertion chcon3i ${⊢}{A}={B}↔\perp \left({B}\right)=\perp \left({A}\right)$

Proof

Step Hyp Ref Expression
1 ch0le.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 chjcl.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 1 2 chsscon3i ${⊢}{A}\subseteq {B}↔\perp \left({B}\right)\subseteq \perp \left({A}\right)$
4 2 1 chsscon3i ${⊢}{B}\subseteq {A}↔\perp \left({A}\right)\subseteq \perp \left({B}\right)$
5 3 4 anbi12i ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)↔\left(\perp \left({B}\right)\subseteq \perp \left({A}\right)\wedge \perp \left({A}\right)\subseteq \perp \left({B}\right)\right)$
6 eqss ${⊢}{A}={B}↔\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$
7 eqss ${⊢}\perp \left({B}\right)=\perp \left({A}\right)↔\left(\perp \left({B}\right)\subseteq \perp \left({A}\right)\wedge \perp \left({A}\right)\subseteq \perp \left({B}\right)\right)$
8 5 6 7 3bitr4i ${⊢}{A}={B}↔\perp \left({B}\right)=\perp \left({A}\right)$