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

Metamath Proof Explorer

Theorem ssdmd1

Description: Ordering implies the dual modular pair property. Remark in MaedaMaeda p. 1. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion ssdmd1 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → A 𝑀 ℋ * B

Proof

Step Hyp Ref Expression
1 choccl ⊢ B ∈ C ℋ → ⊥ ⁡ B ∈ C ℋ
2 choccl ⊢ A ∈ C ℋ → ⊥ ⁡ A ∈ C ℋ
3 ssmd2 ⊢ ⊥ ⁡ B ∈ C ℋ ∧ ⊥ ⁡ A ∈ C ℋ ∧ ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B
4 3 3expia ⊢ ⊥ ⁡ B ∈ C ℋ ∧ ⊥ ⁡ A ∈ C ℋ → ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B
5 1 2 4 syl2anr ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → ⊥ ⁡ B ⊆ ⊥ ⁡ A → ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B
6 chsscon3 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B ↔ ⊥ ⁡ B ⊆ ⊥ ⁡ A
7 dmdmd ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A 𝑀 ℋ * B ↔ ⊥ ⁡ A 𝑀 ℋ ⊥ ⁡ B
8 5 6 7 3imtr4d ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⊆ B → A 𝑀 ℋ * B
9 8 3impia ⊢ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊆ B → A 𝑀 ℋ * B