Metamath Proof Explorer

Theorem genpprecl

Description: Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
genp.2 
|- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
Assertion genpprecl 
|- ( ( A e. P. /\ B e. P. ) -> ( ( C e. A /\ D e. B ) -> ( C G D ) e. ( A F B ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 
 |-  F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )
2 genp.2 
 |-  ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )
3 eqid 
 |-  ( C G D ) = ( C G D )
4 rspceov 
 |-  ( ( C e. A /\ D e. B /\ ( C G D ) = ( C G D ) ) -> E. g e. A E. h e. B ( C G D ) = ( g G h ) )
5 3 4 mp3an3 
 |-  ( ( C e. A /\ D e. B ) -> E. g e. A E. h e. B ( C G D ) = ( g G h ) )
6 1 2 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( C G D ) e. ( A F B ) <-> E. g e. A E. h e. B ( C G D ) = ( g G h ) ) )
7 5 6 imbitrrid 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( C e. A /\ D e. B ) -> ( C G D ) e. ( A F B ) ) )