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

Proof

Step	Hyp	Ref	Expression
1		inss2	|- ( ( x vH B ) i^i A ) C_ A
2		chub2	|- ( ( A e. CH /\ x e. CH ) -> A C_ ( x vH A ) )
3	1 2	sstrid	|- ( ( A e. CH /\ x e. CH ) -> ( ( x vH B ) i^i A ) C_ ( x vH A ) )
4	3	adantrl	|- ( ( A e. CH /\ ( A C_ B /\ x e. CH ) ) -> ( ( x vH B ) i^i A ) C_ ( x vH A ) )
5		simpl	|- ( ( A C_ B /\ x e. CH ) -> A C_ B )
6		sseqin2	|- ( A C_ B <-> ( B i^i A ) = A )
7	5 6	sylib	|- ( ( A C_ B /\ x e. CH ) -> ( B i^i A ) = A )
8	7	adantl	|- ( ( A e. CH /\ ( A C_ B /\ x e. CH ) ) -> ( B i^i A ) = A )
9	8	oveq2d	|- ( ( A e. CH /\ ( A C_ B /\ x e. CH ) ) -> ( x vH ( B i^i A ) ) = ( x vH A ) )
10	4 9	sseqtrrd	|- ( ( A e. CH /\ ( A C_ B /\ x e. CH ) ) -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) )
11	10	a1d	|- ( ( A e. CH /\ ( A C_ B /\ x e. CH ) ) -> ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) )
12	11	exp32	|- ( A e. CH -> ( A C_ B -> ( x e. CH -> ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) ) ) )
13	12	ralrimdv	|- ( A e. CH -> ( A C_ B -> A. x e. CH ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) ) )
14	13	adantr	|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B -> A. x e. CH ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) ) )
15		mdbr2	|- ( ( B e. CH /\ A e. CH ) -> ( B MH A <-> A. x e. CH ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) ) )
16	15	ancoms	|- ( ( A e. CH /\ B e. CH ) -> ( B MH A <-> A. x e. CH ( x C_ A -> ( ( x vH B ) i^i A ) C_ ( x vH ( B i^i A ) ) ) ) )
17	14 16	sylibrd	|- ( ( A e. CH /\ B e. CH ) -> ( A C_ B -> B MH A ) )
18	17	3impia	|- ( ( A e. CH /\ B e. CH /\ A C_ B ) -> B MH A )