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