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

Metamath Proof Explorer

Theorem dmdi4

Description: Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005) (New usage is discouraged.)

Ref Expression
Assertion dmdi4 
|- ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A MH* B -> ( ( C vH B ) i^i ( A vH B ) ) C_ ( ( ( C vH B ) i^i A ) vH B ) ) )

Proof

Step Hyp Ref Expression
1 dmdbr4 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B <-> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
2 1 biimpd 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A MH* B -> A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) ) )
3 oveq1 
 |-  ( x = C -> ( x vH B ) = ( C vH B ) )
4 3 ineq1d 
 |-  ( x = C -> ( ( x vH B ) i^i ( A vH B ) ) = ( ( C vH B ) i^i ( A vH B ) ) )
5 3 ineq1d 
 |-  ( x = C -> ( ( x vH B ) i^i A ) = ( ( C vH B ) i^i A ) )
6 5 oveq1d 
 |-  ( x = C -> ( ( ( x vH B ) i^i A ) vH B ) = ( ( ( C vH B ) i^i A ) vH B ) )
7 4 6 sseq12d 
 |-  ( x = C -> ( ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) <-> ( ( C vH B ) i^i ( A vH B ) ) C_ ( ( ( C vH B ) i^i A ) vH B ) ) )
8 7 rspcv 
 |-  ( C e. CH -> ( A. x e. CH ( ( x vH B ) i^i ( A vH B ) ) C_ ( ( ( x vH B ) i^i A ) vH B ) -> ( ( C vH B ) i^i ( A vH B ) ) C_ ( ( ( C vH B ) i^i A ) vH B ) ) )
9 2 8 sylan9 
 |-  ( ( ( A e. CH /\ B e. CH ) /\ C e. CH ) -> ( A MH* B -> ( ( C vH B ) i^i ( A vH B ) ) C_ ( ( ( C vH B ) i^i A ) vH B ) ) )
10 9 3impa 
 |-  ( ( A e. CH /\ B e. CH /\ C e. CH ) -> ( A MH* B -> ( ( C vH B ) i^i ( A vH B ) ) C_ ( ( ( C vH B ) i^i A ) vH B ) ) )