Step |
Hyp |
Ref |
Expression |
1 |
|
fvopab3ig.1 |
|- ( x = A -> ( ph <-> ps ) ) |
2 |
|
fvopab3ig.2 |
|- ( y = B -> ( ps <-> ch ) ) |
3 |
|
fvopab3ig.3 |
|- ( x e. C -> E* y ph ) |
4 |
|
fvopab3ig.4 |
|- F = { <. x , y >. | ( x e. C /\ ph ) } |
5 |
|
eleq1 |
|- ( x = A -> ( x e. C <-> A e. C ) ) |
6 |
5 1
|
anbi12d |
|- ( x = A -> ( ( x e. C /\ ph ) <-> ( A e. C /\ ps ) ) ) |
7 |
2
|
anbi2d |
|- ( y = B -> ( ( A e. C /\ ps ) <-> ( A e. C /\ ch ) ) ) |
8 |
6 7
|
opelopabg |
|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } <-> ( A e. C /\ ch ) ) ) |
9 |
8
|
biimpar |
|- ( ( ( A e. C /\ B e. D ) /\ ( A e. C /\ ch ) ) -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) |
10 |
9
|
exp43 |
|- ( A e. C -> ( B e. D -> ( A e. C -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) ) ) ) |
11 |
10
|
pm2.43a |
|- ( A e. C -> ( B e. D -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) ) ) |
12 |
11
|
imp |
|- ( ( A e. C /\ B e. D ) -> ( ch -> <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } ) ) |
13 |
4
|
fveq1i |
|- ( F ` A ) = ( { <. x , y >. | ( x e. C /\ ph ) } ` A ) |
14 |
|
funopab |
|- ( Fun { <. x , y >. | ( x e. C /\ ph ) } <-> A. x E* y ( x e. C /\ ph ) ) |
15 |
|
moanimv |
|- ( E* y ( x e. C /\ ph ) <-> ( x e. C -> E* y ph ) ) |
16 |
3 15
|
mpbir |
|- E* y ( x e. C /\ ph ) |
17 |
14 16
|
mpgbir |
|- Fun { <. x , y >. | ( x e. C /\ ph ) } |
18 |
|
funopfv |
|- ( Fun { <. x , y >. | ( x e. C /\ ph ) } -> ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( { <. x , y >. | ( x e. C /\ ph ) } ` A ) = B ) ) |
19 |
17 18
|
ax-mp |
|- ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( { <. x , y >. | ( x e. C /\ ph ) } ` A ) = B ) |
20 |
13 19
|
eqtrid |
|- ( <. A , B >. e. { <. x , y >. | ( x e. C /\ ph ) } -> ( F ` A ) = B ) |
21 |
12 20
|
syl6 |
|- ( ( A e. C /\ B e. D ) -> ( ch -> ( F ` A ) = B ) ) |