Metamath Proof Explorer

Theorem afvco2

Description: Value of a function composition, analogous to fvco2 . (Contributed by Alexander van der Vekens, 23-Jul-2017)

Ref Expression
Assertion afvco2 
|- ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = ( F ''' ( G ''' X ) ) )

Proof

Step Hyp Ref Expression
1 fvco2 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
2 1 adantl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
3 simpll 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( G ` X ) e. dom F )
4 df-fn 
 |-  ( G Fn A <-> ( Fun G /\ dom G = A ) )
5 simpll 
 |-  ( ( ( Fun G /\ dom G = A ) /\ X e. A ) -> Fun G )
6 eleq2 
 |-  ( A = dom G -> ( X e. A <-> X e. dom G ) )
7 6 eqcoms 
 |-  ( dom G = A -> ( X e. A <-> X e. dom G ) )
8 7 biimpd 
 |-  ( dom G = A -> ( X e. A -> X e. dom G ) )
9 8 adantl 
 |-  ( ( Fun G /\ dom G = A ) -> ( X e. A -> X e. dom G ) )
10 9 imp 
 |-  ( ( ( Fun G /\ dom G = A ) /\ X e. A ) -> X e. dom G )
11 5 10 jca 
 |-  ( ( ( Fun G /\ dom G = A ) /\ X e. A ) -> ( Fun G /\ X e. dom G ) )
12 4 11 sylanb 
 |-  ( ( G Fn A /\ X e. A ) -> ( Fun G /\ X e. dom G ) )
13 12 adantl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( Fun G /\ X e. dom G ) )
14 dmfco 
 |-  ( ( Fun G /\ X e. dom G ) -> ( X e. dom ( F o. G ) <-> ( G ` X ) e. dom F ) )
15 13 14 syl 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( X e. dom ( F o. G ) <-> ( G ` X ) e. dom F ) )
16 3 15 mpbird 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> X e. dom ( F o. G ) )
17 funcoressn 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( ( F o. G ) |` { X } ) )
18 df-dfat 
 |-  ( ( F o. G ) defAt X <-> ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) )
19 afvfundmfveq 
 |-  ( ( F o. G ) defAt X -> ( ( F o. G ) ''' X ) = ( ( F o. G ) ` X ) )
20 18 19 sylbir 
 |-  ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) -> ( ( F o. G ) ''' X ) = ( ( F o. G ) ` X ) )
21 16 17 20 syl2anc 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F o. G ) ''' X ) = ( ( F o. G ) ` X ) )
22 df-dfat 
 |-  ( F defAt ( G ` X ) <-> ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) )
23 afvfundmfveq 
 |-  ( F defAt ( G ` X ) -> ( F ''' ( G ` X ) ) = ( F ` ( G ` X ) ) )
24 22 23 sylbir 
 |-  ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) -> ( F ''' ( G ` X ) ) = ( F ` ( G ` X ) ) )
25 24 adantr 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( F ''' ( G ` X ) ) = ( F ` ( G ` X ) ) )
26 2 21 25 3eqtr4d 
 |-  ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F o. G ) ''' X ) = ( F ''' ( G ` X ) ) )
27 ianor 
 |-  ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) <-> ( -. ( G ` X ) e. dom F \/ -. Fun ( F |` { ( G ` X ) } ) ) )
28 14 funfni 
 |-  ( ( G Fn A /\ X e. A ) -> ( X e. dom ( F o. G ) <-> ( G ` X ) e. dom F ) )
29 28 bicomd 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( G ` X ) e. dom F <-> X e. dom ( F o. G ) ) )
30 29 notbid 
 |-  ( ( G Fn A /\ X e. A ) -> ( -. ( G ` X ) e. dom F <-> -. X e. dom ( F o. G ) ) )
31 30 biimpd 
 |-  ( ( G Fn A /\ X e. A ) -> ( -. ( G ` X ) e. dom F -> -. X e. dom ( F o. G ) ) )
32 ndmafv 
 |-  ( -. X e. dom ( F o. G ) -> ( ( F o. G ) ''' X ) = _V )
33 31 32 syl6com 
 |-  ( -. ( G ` X ) e. dom F -> ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = _V ) )
34 funressnfv 
 |-  ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( F |` { ( G ` X ) } ) )
35 34 ex 
 |-  ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) -> ( ( G Fn A /\ X e. A ) -> Fun ( F |` { ( G ` X ) } ) ) )
36 afvnfundmuv 
 |-  ( -. ( F o. G ) defAt X -> ( ( F o. G ) ''' X ) = _V )
37 18 36 sylnbir 
 |-  ( -. ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) -> ( ( F o. G ) ''' X ) = _V )
38 35 37 nsyl4 
 |-  ( -. ( ( F o. G ) ''' X ) = _V -> ( ( G Fn A /\ X e. A ) -> Fun ( F |` { ( G ` X ) } ) ) )
39 38 com12 
 |-  ( ( G Fn A /\ X e. A ) -> ( -. ( ( F o. G ) ''' X ) = _V -> Fun ( F |` { ( G ` X ) } ) ) )
40 39 con1d 
 |-  ( ( G Fn A /\ X e. A ) -> ( -. Fun ( F |` { ( G ` X ) } ) -> ( ( F o. G ) ''' X ) = _V ) )
41 40 com12 
 |-  ( -. Fun ( F |` { ( G ` X ) } ) -> ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = _V ) )
42 33 41 jaoi 
 |-  ( ( -. ( G ` X ) e. dom F \/ -. Fun ( F |` { ( G ` X ) } ) ) -> ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = _V ) )
43 27 42 sylbi 
 |-  ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) -> ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = _V ) )
44 43 imp 
 |-  ( ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F o. G ) ''' X ) = _V )
45 afvnfundmuv 
 |-  ( -. F defAt ( G ` X ) -> ( F ''' ( G ` X ) ) = _V )
46 22 45 sylnbir 
 |-  ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) -> ( F ''' ( G ` X ) ) = _V )
47 46 eqcomd 
 |-  ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) -> _V = ( F ''' ( G ` X ) ) )
48 47 adantr 
 |-  ( ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> _V = ( F ''' ( G ` X ) ) )
49 44 48 eqtrd 
 |-  ( ( -. ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> ( ( F o. G ) ''' X ) = ( F ''' ( G ` X ) ) )
50 26 49 pm2.61ian 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = ( F ''' ( G ` X ) ) )
51 eqidd 
 |-  ( ( G Fn A /\ X e. A ) -> F = F )
52 4 9 sylbi 
 |-  ( G Fn A -> ( X e. A -> X e. dom G ) )
53 52 imp 
 |-  ( ( G Fn A /\ X e. A ) -> X e. dom G )
54 fnfun 
 |-  ( G Fn A -> Fun G )
55 funres 
 |-  ( Fun G -> Fun ( G |` { X } ) )
56 54 55 syl 
 |-  ( G Fn A -> Fun ( G |` { X } ) )
57 56 adantr 
 |-  ( ( G Fn A /\ X e. A ) -> Fun ( G |` { X } ) )
58 df-dfat 
 |-  ( G defAt X <-> ( X e. dom G /\ Fun ( G |` { X } ) ) )
59 afvfundmfveq 
 |-  ( G defAt X -> ( G ''' X ) = ( G ` X ) )
60 58 59 sylbir 
 |-  ( ( X e. dom G /\ Fun ( G |` { X } ) ) -> ( G ''' X ) = ( G ` X ) )
61 53 57 60 syl2anc 
 |-  ( ( G Fn A /\ X e. A ) -> ( G ''' X ) = ( G ` X ) )
62 61 eqcomd 
 |-  ( ( G Fn A /\ X e. A ) -> ( G ` X ) = ( G ''' X ) )
63 51 62 afveq12d 
 |-  ( ( G Fn A /\ X e. A ) -> ( F ''' ( G ` X ) ) = ( F ''' ( G ''' X ) ) )
64 50 63 eqtrd 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ''' X ) = ( F ''' ( G ''' X ) ) )