# 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 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{𝑀}_{ℋ}^{*}{B}$

### Proof

Step Hyp Ref Expression
1 choccl ${⊢}{B}\in {\mathbf{C}}_{ℋ}\to \perp \left({B}\right)\in {\mathbf{C}}_{ℋ}$
2 choccl ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}$
3 ssmd2 ${⊢}\left(\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({B}\right)\subseteq \perp \left({A}\right)\right)\to \perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)$
4 3 3expia ${⊢}\left(\perp \left({B}\right)\in {\mathbf{C}}_{ℋ}\wedge \perp \left({A}\right)\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({B}\right)\subseteq \perp \left({A}\right)\to \perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$
5 1 2 4 syl2anr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left(\perp \left({B}\right)\subseteq \perp \left({A}\right)\to \perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$
6 chsscon3 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}↔\perp \left({B}\right)\subseteq \perp \left({A}\right)\right)$
7 dmdmd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}^{*}{B}↔\perp \left({A}\right){𝑀}_{ℋ}\perp \left({B}\right)\right)$
8 5 6 7 3imtr4d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {A}{𝑀}_{ℋ}^{*}{B}\right)$
9 8 3impia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{𝑀}_{ℋ}^{*}{B}$