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

Metamath Proof Explorer

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 imbitrrid 
 |-  ( ( 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 )