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. )