Step |
Hyp |
Ref |
Expression |
1 |
|
eldm2g |
|- ( A e. dom G -> ( A e. dom ( F o. G ) <-> E. y <. A , y >. e. ( F o. G ) ) ) |
2 |
|
opelco2g |
|- ( ( A e. dom G /\ y e. _V ) -> ( <. A , y >. e. ( F o. G ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
3 |
2
|
elvd |
|- ( A e. dom G -> ( <. A , y >. e. ( F o. G ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
4 |
3
|
exbidv |
|- ( A e. dom G -> ( E. y <. A , y >. e. ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
5 |
1 4
|
bitrd |
|- ( A e. dom G -> ( A e. dom ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
6 |
5
|
adantl |
|- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
7 |
|
fvex |
|- ( G ` A ) e. _V |
8 |
7
|
eldm2 |
|- ( ( G ` A ) e. dom F <-> E. y <. ( G ` A ) , y >. e. F ) |
9 |
|
opeq1 |
|- ( x = ( G ` A ) -> <. x , y >. = <. ( G ` A ) , y >. ) |
10 |
9
|
eleq1d |
|- ( x = ( G ` A ) -> ( <. x , y >. e. F <-> <. ( G ` A ) , y >. e. F ) ) |
11 |
7 10
|
ceqsexv |
|- ( E. x ( x = ( G ` A ) /\ <. x , y >. e. F ) <-> <. ( G ` A ) , y >. e. F ) |
12 |
|
eqcom |
|- ( x = ( G ` A ) <-> ( G ` A ) = x ) |
13 |
|
funopfvb |
|- ( ( Fun G /\ A e. dom G ) -> ( ( G ` A ) = x <-> <. A , x >. e. G ) ) |
14 |
12 13
|
syl5bb |
|- ( ( Fun G /\ A e. dom G ) -> ( x = ( G ` A ) <-> <. A , x >. e. G ) ) |
15 |
14
|
anbi1d |
|- ( ( Fun G /\ A e. dom G ) -> ( ( x = ( G ` A ) /\ <. x , y >. e. F ) <-> ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
16 |
15
|
exbidv |
|- ( ( Fun G /\ A e. dom G ) -> ( E. x ( x = ( G ` A ) /\ <. x , y >. e. F ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
17 |
11 16
|
bitr3id |
|- ( ( Fun G /\ A e. dom G ) -> ( <. ( G ` A ) , y >. e. F <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
18 |
17
|
exbidv |
|- ( ( Fun G /\ A e. dom G ) -> ( E. y <. ( G ` A ) , y >. e. F <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
19 |
8 18
|
syl5bb |
|- ( ( Fun G /\ A e. dom G ) -> ( ( G ` A ) e. dom F <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) ) |
20 |
6 19
|
bitr4d |
|- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> ( G ` A ) e. dom F ) ) |