This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )