Metamath Proof Explorer

Theorem genpn0

Description: The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-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 genpn0 
|- ( ( A e. P. /\ B e. P. ) -> (/) C. ( 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 prn0 
 |-  ( A e. P. -> A =/= (/) )
4 n0 
 |-  ( A =/= (/) <-> E. f f e. A )
5 3 4 sylib 
 |-  ( A e. P. -> E. f f e. A )
6 prn0 
 |-  ( B e. P. -> B =/= (/) )
7 n0 
 |-  ( B =/= (/) <-> E. g g e. B )
8 6 7 sylib 
 |-  ( B e. P. -> E. g g e. B )
9 5 8 anim12i 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. f f e. A /\ E. g g e. B ) )
10 1 2 genpprecl 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( f e. A /\ g e. B ) -> ( f G g ) e. ( A F B ) ) )
11 ne0i 
 |-  ( ( f G g ) e. ( A F B ) -> ( A F B ) =/= (/) )
12 0pss 
 |-  ( (/) C. ( A F B ) <-> ( A F B ) =/= (/) )
13 11 12 sylibr 
 |-  ( ( f G g ) e. ( A F B ) -> (/) C. ( A F B ) )
14 10 13 syl6 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( f e. A /\ g e. B ) -> (/) C. ( A F B ) ) )
15 14 expcomd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( g e. B -> ( f e. A -> (/) C. ( A F B ) ) ) )
16 15 exlimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. g g e. B -> ( f e. A -> (/) C. ( A F B ) ) ) )
17 16 com23 
 |-  ( ( A e. P. /\ B e. P. ) -> ( f e. A -> ( E. g g e. B -> (/) C. ( A F B ) ) ) )
18 17 exlimdv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( E. f f e. A -> ( E. g g e. B -> (/) C. ( A F B ) ) ) )
19 18 impd 
 |-  ( ( A e. P. /\ B e. P. ) -> ( ( E. f f e. A /\ E. g g e. B ) -> (/) C. ( A F B ) ) )
20 9 19 mpd 
 |-  ( ( A e. P. /\ B e. P. ) -> (/) C. ( A F B ) )