This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chpsscon2

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

Ref Expression
Assertion chpsscon2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊂ ⊥ ⁡ B ↔ B ⊂ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 choccl ⊢ B ∈ C ℋ → ⊥ ⁡ B ∈ C ℋ
2 chpsscon3 ⊢ A ∈ C ℋ ∧ ⊥ ⁡ B ∈ C ℋ → A ⊂ ⊥ ⁡ B ↔ ⊥ ⁡ ⊥ ⁡ B ⊂ ⊥ ⁡ A
3 1 2 sylan2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊂ ⊥ ⁡ B ↔ ⊥ ⁡ ⊥ ⁡ B ⊂ ⊥ ⁡ A
4 ococ ⊢ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ B = B
5 4 adantl ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ B = B
6 5 psseq1d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ B ⊂ ⊥ ⁡ A ↔ B ⊂ ⊥ ⁡ A
7 3 6 bitrd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊂ ⊥ ⁡ B ↔ B ⊂ ⊥ ⁡ A