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		simpl	$$⊢\left(A\subseteq B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to A\subseteq B$$
6		sseqin2	$$⊢A\subseteq B\leftrightarrow B\cap A=A$$
7	5 6	sylib	$$⊢\left(A\subseteq B\wedge x\in {\mathbf{C}}_{\mathscr{H}}\right)\to B\cap A=A$$
8	7	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$$
9	8	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$$
10	4 9	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)$$
11	10	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)$$
12	11	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)$$
13	12	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)$$
14	13	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)$$
15		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)$$
16	15	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)$$
17	14 16	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)$$
18	17	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$$