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	|- ( ( A e. CH /\ B e. CH /\ A C_ B ) -> A MH B )

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( ( x vH A ) i^i B ) C_ ( x vH A )
2		dfss	|- ( A C_ B <-> A = ( A i^i B ) )
3	2	biimpi	|- ( A C_ B -> A = ( A i^i B ) )
4	3	oveq2d	|- ( A C_ B -> ( x vH A ) = ( x vH ( A i^i B ) ) )
5	1 4	sseqtrid	|- ( A C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) )
6	5	a1d	|- ( A C_ B -> ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
7	6	ralrimivw	|- ( A C_ B -> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) )
8		mdbr2	|- ( ( A e. CH /\ B e. CH ) -> ( A MH B <-> A. x e. CH ( x C_ B -> ( ( x vH A ) i^i B ) C_ ( x vH ( A i^i B ) ) ) ) )
9	7 8	syl5ibr	|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B -> A MH B ) )
10	9	3impia	|- ( ( A e. CH /\ B e. CH /\ A C_ B ) -> A MH B )