Metamath Proof Explorer

Theorem chsscon3i

Description: Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 ⊢ A ∈ C ℋ
chjcl.2 ⊢ B ∈ C ℋ
Assertion chsscon3i ⊢ A ⊆ B ↔ ⊥ ⁡ B ⊆ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 ch0le.1 ⊢ A ∈ C ℋ
2 chjcl.2 ⊢ B ∈ C ℋ
3 1 chssii ⊢ A ⊆ ℋ
4 2 chssii ⊢ B ⊆ ℋ
5 occon ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A
6 3 4 5 mp2an ⊢ A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A
7 2 choccli ⊢ ⊥ ⁡ B ∈ C ℋ
8 7 chssii ⊢ ⊥ ⁡ B ⊆ ℋ
9 1 choccli ⊢ ⊥ ⁡ A ∈ C ℋ
10 9 chssii ⊢ ⊥ ⁡ A ⊆ ℋ
11 occon ⊢ ⊥ ⁡ B ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ B
12 8 10 11 mp2an ⊢ ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ B
13 1 pjococi ⊢ ⊥ ⁡ ⊥ ⁡ A = A
14 2 pjococi ⊢ ⊥ ⁡ ⊥ ⁡ B = B
15 12 13 14 3sstr3g ⊢ ⊥ ⁡ B ⊆ ⊥ ⁡ A → A ⊆ B
16 6 15 impbii ⊢ A ⊆ B ↔ ⊥ ⁡ B ⊆ ⊥ ⁡ A