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 ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐹 ∘ 𝐺 ) ''' 𝑋 ) = ( 𝐹 ''' ( 𝐺 ''' 𝑋 ) ) )

Proof

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