Metamath Proof Explorer

Theorem dfatdmfcoafv2

Description: Domain of a function composition, analogous to dmfco . (Contributed by AV, 7-Sep-2022)

Ref Expression
Assertion dfatdmfcoafv2 
|- ( G defAt A -> ( A e. dom ( F o. G ) <-> ( G '''' A ) e. dom F ) )

Proof

Step Hyp Ref Expression
1 dfatafv2ex 
 |-  ( G defAt A -> ( G '''' A ) e. _V )
2 opeq1 
 |-  ( x = ( G '''' A ) -> <. x , y >. = <. ( G '''' A ) , y >. )
3 2 eleq1d 
 |-  ( x = ( G '''' A ) -> ( <. x , y >. e. F <-> <. ( G '''' A ) , y >. e. F ) )
4 3 ceqsexgv 
 |-  ( ( G '''' A ) e. _V -> ( E. x ( x = ( G '''' A ) /\ <. x , y >. e. F ) <-> <. ( G '''' A ) , y >. e. F ) )
5 4 bicomd 
 |-  ( ( G '''' A ) e. _V -> ( <. ( G '''' A ) , y >. e. F <-> E. x ( x = ( G '''' A ) /\ <. x , y >. e. F ) ) )
6 1 5 syl 
 |-  ( G defAt A -> ( <. ( G '''' A ) , y >. e. F <-> E. x ( x = ( G '''' A ) /\ <. x , y >. e. F ) ) )
7 eqcom 
 |-  ( x = ( G '''' A ) <-> ( G '''' A ) = x )
8 dfatopafv2b 
 |-  ( ( G defAt A /\ x e. _V ) -> ( ( G '''' A ) = x <-> <. A , x >. e. G ) )
9 8 elvd 
 |-  ( G defAt A -> ( ( G '''' A ) = x <-> <. A , x >. e. G ) )
10 7 9 bitrid 
 |-  ( G defAt A -> ( x = ( G '''' A ) <-> <. A , x >. e. G ) )
11 10 anbi1d 
 |-  ( G defAt A -> ( ( x = ( G '''' A ) /\ <. x , y >. e. F ) <-> ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
12 11 exbidv 
 |-  ( G defAt A -> ( E. x ( x = ( G '''' A ) /\ <. x , y >. e. F ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
13 6 12 bitrd 
 |-  ( G defAt A -> ( <. ( G '''' A ) , y >. e. F <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
14 13 exbidv 
 |-  ( G defAt A -> ( E. y <. ( G '''' A ) , y >. e. F <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
15 eldm2g 
 |-  ( ( G '''' A ) e. _V -> ( ( G '''' A ) e. dom F <-> E. y <. ( G '''' A ) , y >. e. F ) )
16 1 15 syl 
 |-  ( G defAt A -> ( ( G '''' A ) e. dom F <-> E. y <. ( G '''' A ) , y >. e. F ) )
17 df-dfat 
 |-  ( G defAt A <-> ( A e. dom G /\ Fun ( G |` { A } ) ) )
18 eldm2g 
 |-  ( A e. dom G -> ( A e. dom ( F o. G ) <-> E. y <. A , y >. e. ( F o. G ) ) )
19 opelco2g 
 |-  ( ( A e. dom G /\ y e. _V ) -> ( <. A , y >. e. ( F o. G ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
20 19 elvd 
 |-  ( A e. dom G -> ( <. A , y >. e. ( F o. G ) <-> E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
21 20 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 ) ) )
22 18 21 bitrd 
 |-  ( A e. dom G -> ( A e. dom ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
23 22 adantr 
 |-  ( ( A e. dom G /\ Fun ( G |` { A } ) ) -> ( A e. dom ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
24 17 23 sylbi 
 |-  ( G defAt A -> ( A e. dom ( F o. G ) <-> E. y E. x ( <. A , x >. e. G /\ <. x , y >. e. F ) ) )
25 14 16 24 3bitr4rd 
 |-  ( G defAt A -> ( A e. dom ( F o. G ) <-> ( G '''' A ) e. dom F ) )