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
|
genpv |
|- ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { f | E. g e. A E. h e. B f = ( g G h ) } ) |
4 |
3
|
eleq2d |
|- ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> C e. { f | E. g e. A E. h e. B f = ( g G h ) } ) ) |
5 |
|
id |
|- ( C = ( g G h ) -> C = ( g G h ) ) |
6 |
|
ovex |
|- ( g G h ) e. _V |
7 |
5 6
|
eqeltrdi |
|- ( C = ( g G h ) -> C e. _V ) |
8 |
7
|
rexlimivw |
|- ( E. h e. B C = ( g G h ) -> C e. _V ) |
9 |
8
|
rexlimivw |
|- ( E. g e. A E. h e. B C = ( g G h ) -> C e. _V ) |
10 |
|
eqeq1 |
|- ( f = C -> ( f = ( g G h ) <-> C = ( g G h ) ) ) |
11 |
10
|
2rexbidv |
|- ( f = C -> ( E. g e. A E. h e. B f = ( g G h ) <-> E. g e. A E. h e. B C = ( g G h ) ) ) |
12 |
9 11
|
elab3 |
|- ( C e. { f | E. g e. A E. h e. B f = ( g G h ) } <-> E. g e. A E. h e. B C = ( g G h ) ) |
13 |
4 12
|
bitrdi |
|- ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> E. g e. A E. h e. B C = ( g G h ) ) ) |