# Metamath Proof Explorer

## Theorem ssmd1

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

Ref Expression
Assertion ssmd1 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{𝑀}_{ℋ}{B}$

### Proof

Step Hyp Ref Expression
1 inss1 ${⊢}\left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}{A}$
2 dfss ${⊢}{A}\subseteq {B}↔{A}={A}\cap {B}$
3 2 biimpi ${⊢}{A}\subseteq {B}\to {A}={A}\cap {B}$
4 3 oveq2d ${⊢}{A}\subseteq {B}\to {x}{\vee }_{ℋ}{A}={x}{\vee }_{ℋ}\left({A}\cap {B}\right)$
5 1 4 sseqtrid ${⊢}{A}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)$
6 5 a1d ${⊢}{A}\subseteq {B}\to \left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
7 6 ralrimivw ${⊢}{A}\subseteq {B}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)$
8 mdbr2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}{𝑀}_{ℋ}{B}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {B}\to \left({x}{\vee }_{ℋ}{A}\right)\cap {B}\subseteq {x}{\vee }_{ℋ}\left({A}\cap {B}\right)\right)\right)$
9 7 8 syl5ibr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {A}{𝑀}_{ℋ}{B}\right)$
10 9 3impia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {A}{𝑀}_{ℋ}{B}$