Metamath Proof Explorer

Theorem funcoressn

Description: A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017)

Ref Expression
Assertion funcoressn ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) )

Proof

Step Hyp Ref Expression
1 dmressnsn ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 → dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } )
2 df-fn ⊢ ( ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } ↔ ( Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ∧ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } ) )
3 2 simplbi2com ⊢ ( dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } → ( Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } ) )
4 1 3 syl ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 → ( Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } ) )
5 4 imp ⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) → ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } )
6 5 adantr ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } )
7 fnsnfv ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → { ( 𝐺 ‘ 𝑋 ) } = ( 𝐺 “ { 𝑋 } ) )
8 7 adantl ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → { ( 𝐺 ‘ 𝑋 ) } = ( 𝐺 “ { 𝑋 } ) )
9 df-ima ⊢ ( 𝐺 “ { 𝑋 } ) = ran ( 𝐺 ↾ { 𝑋 } )
10 8 9 eqtrdi ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → { ( 𝐺 ‘ 𝑋 ) } = ran ( 𝐺 ↾ { 𝑋 } ) )
11 10 reseq2d ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = ( 𝐹 ↾ ran ( 𝐺 ↾ { 𝑋 } ) ) )
12 11 10 fneq12d ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) Fn { ( 𝐺 ‘ 𝑋 ) } ↔ ( 𝐹 ↾ ran ( 𝐺 ↾ { 𝑋 } ) ) Fn ran ( 𝐺 ↾ { 𝑋 } ) ) )
13 6 12 mpbid ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐹 ↾ ran ( 𝐺 ↾ { 𝑋 } ) ) Fn ran ( 𝐺 ↾ { 𝑋 } ) )
14 fnfun ⊢ ( 𝐺 Fn 𝐴 → Fun 𝐺 )
15 funres ⊢ ( Fun 𝐺 → Fun ( 𝐺 ↾ { 𝑋 } ) )
16 15 funfnd ⊢ ( Fun 𝐺 → ( 𝐺 ↾ { 𝑋 } ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
17 14 16 syl ⊢ ( 𝐺 Fn 𝐴 → ( 𝐺 ↾ { 𝑋 } ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
18 17 adantr ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐺 ↾ { 𝑋 } ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
19 18 adantl ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐺 ↾ { 𝑋 } ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
20 fnresfnco ⊢ ( ( ( 𝐹 ↾ ran ( 𝐺 ↾ { 𝑋 } ) ) Fn ran ( 𝐺 ↾ { 𝑋 } ) ∧ ( 𝐺 ↾ { 𝑋 } ) Fn dom ( 𝐺 ↾ { 𝑋 } ) ) → ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
21 13 19 20 syl2anc ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) Fn dom ( 𝐺 ↾ { 𝑋 } ) )
22 fnfun ⊢ ( ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) Fn dom ( 𝐺 ↾ { 𝑋 } ) → Fun ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) )
23 21 22 syl ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → Fun ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) )
24 resco ⊢ ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) )
25 24 funeqi ⊢ ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ↔ Fun ( 𝐹 ∘ ( 𝐺 ↾ { 𝑋 } ) ) )
26 23 25 sylibr ⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) )