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

Metamath Proof Explorer

Theorem occon2

Description: Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ocss ⊢ A ⊆ ℋ → ⊥ ⁡ A ⊆ ℋ
2 ocss ⊢ B ⊆ ℋ → ⊥ ⁡ B ⊆ ℋ
3 1 2 anim12ci ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → ⊥ ⁡ B ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ
4 occon ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ B ⊆ ⊥ ⁡ A
5 occon ⊢ ⊥ ⁡ B ⊆ ℋ ∧ ⊥ ⁡ A ⊆ ℋ → ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ B
6 3 4 5 sylsyld ⊢ A ⊆ ℋ ∧ B ⊆ ℋ → A ⊆ B → ⊥ ⁡ ⊥ ⁡ A ⊆ ⊥ ⁡ ⊥ ⁡ B