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

Proof

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