Metamath Proof Explorer

Theorem occon3

Description: Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014) (New usage is discouraged.)

Ref Expression
Assertion occon3 ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ ⊥ ⁡ B ↔ B ⊆ ⊥ ⁡ A

Proof

Step Hyp Ref Expression
1 ococss ⊢ B ⊆ ℋ → B ⊆ ⊥ ⁡ ⊥ ⁡ B
2 1 adantl ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → B ⊆ ⊥ ⁡ ⊥ ⁡ B
3 ocss ⊢ B ⊆ ℋ → ⊥ ⁡ B ⊆ ℋ
4 occon ⊢ A ⊆ ℋ ∧ ⊥ ⁡ B ⊆ ℋ → A ⊆ ⊥ ⁡ B → ⊥ ⁡ ⊥ ⁡ B ⊆ ⊥ ⁡ A
5 3 4 sylan2 ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ ⊥ ⁡ B → ⊥ ⁡ ⊥ ⁡ B ⊆ ⊥ ⁡ A
6 sstr2 ⊢ B ⊆ ⊥ ⁡ ⊥ ⁡ B → ⊥ ⁡ ⊥ ⁡ B ⊆ ⊥ ⁡ A → B ⊆ ⊥ ⁡ A
7 2 5 6 sylsyld ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ ⊥ ⁡ B → B ⊆ ⊥ ⁡ A
8 ococss ⊢ A ⊆ ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ A
9 8 adantr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ ⊥ ⁡ ⊥ ⁡ A
10 id ⊢ B ⊆ ℋ → B ⊆ ℋ
11 ocss ⊢ A ⊆ ℋ → ⊥ ⁡ A ⊆ ℋ
12 occon ⊢ B ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ → B ⊆ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ B
13 10 11 12 syl2anr ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → B ⊆ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ B
14 sstr2 ⊢ A ⊆ ⊥ ⁡ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ B → A ⊆ ⊥ ⁡ B
15 9 13 14 sylsyld ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → B ⊆ ⊥ ⁡ A → A ⊆ ⊥ ⁡ B
16 7 15 impbid ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ ⊥ ⁡ B ↔ B ⊆ ⊥ ⁡ A