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

Metamath Proof Explorer

Theorem genpss

Description: The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995) (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 genpss 
|- ( ( A e. P. /\ B e. P. ) -> ( A F B ) C_ Q. )

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 1 2 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) <-> E. g e. A E. h e. B f = ( g G h ) ) )
4 elprnq 
 |-  ( ( A e. P. /\ g e. A ) -> g e. Q. )
5 4 ex 
 |-  ( A e. P. -> ( g e. A -> g e. Q. ) )
6 elprnq 
 |-  ( ( B e. P. /\ h e. B ) -> h e. Q. )
7 6 ex 
 |-  ( B e. P. -> ( h e. B -> h e. Q. ) )
8 5 7 im2anan9 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( g e. A /\ h e. B ) -> ( g e. Q. /\ h e. Q. ) ) )
9 2 caovcl 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g G h ) e. Q. )
10 8 9 syl6 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( g e. A /\ h e. B ) -> ( g G h ) e. Q. ) )
11 eleq1a 
 |-  ( ( g G h ) e. Q. -> ( f = ( g G h ) -> f e. Q. ) )
12 10 11 syl6 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( g e. A /\ h e. B ) -> ( f = ( g G h ) -> f e. Q. ) ) )
13 12 rexlimdvv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. g e. A E. h e. B f = ( g G h ) -> f e. Q. ) )
14 3 13 sylbid 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> f e. Q. ) )
15 14 ssrdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A F B ) C_ Q. )