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}}_{\mathscr{H}}\wedge B\in {\mathbf{C}}_{\mathscr{H}}\wedge A\subseteq B\right)\to A{𝑀}_{\mathscr{H}}B$$

Proof

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