Metamath Proof Explorer

Theorem dmfco

Description: Domains of a function composition. (Contributed by NM, 27-Jan-1997)

Ref Expression
Assertion dmfco 
|- ( ( Fun G /\ A e. dom G ) -> ( A e. dom ( F o. G ) <-> ( G ` A ) e. dom F ) )

Proof

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