# Metamath Proof Explorer

## Theorem ssmd2

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

### Proof

Step Hyp Ref Expression
1 inss2 ${⊢}\left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {A}$
2 chub2 ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {x}{\vee }_{ℋ}{A}$
3 1 2 sstrid ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}{A}$
4 3 adantrl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}{A}$
5 simpl ${⊢}\left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {A}\subseteq {B}$
6 sseqin2 ${⊢}{A}\subseteq {B}↔{B}\cap {A}={A}$
7 5 6 sylib ${⊢}\left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {B}\cap {A}={A}$
8 7 adantl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\right)\to {B}\cap {A}={A}$
9 8 oveq2d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\right)\to {x}{\vee }_{ℋ}\left({B}\cap {A}\right)={x}{\vee }_{ℋ}{A}$
10 4 9 sseqtrrd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\right)\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)$
11 10 a1d ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge \left({A}\subseteq {B}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\right)\to \left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)$
12 11 exp32 ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left({A}\subseteq {B}\to \left({x}\in {\mathbf{C}}_{ℋ}\to \left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)\right)\right)$
13 12 ralrimdv ${⊢}{A}\in {\mathbf{C}}_{ℋ}\to \left({A}\subseteq {B}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)\right)$
14 13 adantr ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to \forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)\right)$
15 mdbr2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}{𝑀}_{ℋ}{A}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)\right)$
16 15 ancoms ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}{𝑀}_{ℋ}{A}↔\forall {x}\in {\mathbf{C}}_{ℋ}\phantom{\rule{.4em}{0ex}}\left({x}\subseteq {A}\to \left({x}{\vee }_{ℋ}{B}\right)\cap {A}\subseteq {x}{\vee }_{ℋ}\left({B}\cap {A}\right)\right)\right)$
17 14 16 sylibrd ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to \left({A}\subseteq {B}\to {B}{𝑀}_{ℋ}{A}\right)$
18 17 3impia ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\wedge {A}\subseteq {B}\right)\to {B}{𝑀}_{ℋ}{A}$