Metamath Proof Explorer

Theorem chsscon1

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

Ref Expression
Assertion chsscon1 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A ⊆ B ↔ ⊥ ⁡ B ⊆ A

Proof

Step Hyp Ref Expression
1 choccl ⊢ A ∈ C ℋ → ⊥ ⁡ A ∈ C ℋ
2 chsscon3 ⊢ ⊥ ⁡ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A ⊆ B ↔ ⊥ ⁡ B ⊆ ⊥ ⁡ ⊥ ⁡ A
3 1 2 sylan ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A ⊆ B ↔ ⊥ ⁡ B ⊆ ⊥ ⁡ ⊥ ⁡ A
4 ococ ⊢ A ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ A = A
5 4 adantr ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ ⊥ ⁡ A = A
6 5 sseq2d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ B ⊆ ⊥ ⁡ ⊥ ⁡ A ↔ ⊥ ⁡ B ⊆ A
7 3 6 bitrd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ A ⊆ B ↔ ⊥ ⁡ B ⊆ A