Metamath Proof Explorer

Theorem funressnfv

Description: A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } )
2 1 a1i ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → Rel ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) )
3 dmfco ⊢ ( ( Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺 ) → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ) )
4 3 biimpd ⊢ ( ( Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺 ) → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ) )
5 4 funfni ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 ) )
6 dmressnsn ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 → dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } )
7 eleq2 ⊢ ( dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ↔ 𝑥 ∈ { ( 𝐺 ‘ 𝑋 ) } ) )
8 velsn ⊢ ( 𝑥 ∈ { ( 𝐺 ‘ 𝑋 ) } ↔ 𝑥 = ( 𝐺 ‘ 𝑋 ) )
9 dmressnsn ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } )
10 dffun7 ⊢ ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ↔ ( Rel ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ∧ ∀ 𝑥 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
11 snidg ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → 𝑋 ∈ { 𝑋 } )
12 11 adantl ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → 𝑋 ∈ { 𝑋 } )
13 eleq2 ⊢ ( { 𝑋 } = dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) → ( 𝑋 ∈ { 𝑋 } ↔ 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) )
14 13 eqcoms ⊢ ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } → ( 𝑋 ∈ { 𝑋 } ↔ 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) )
15 14 adantr ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( 𝑋 ∈ { 𝑋 } ↔ 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) )
16 12 15 mpbid ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → 𝑋 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) )
17 fvex ⊢ ( 𝐺 ‘ 𝑋 ) ∈ V
18 17 isseti ⊢ ∃ 𝑧 𝑧 = ( 𝐺 ‘ 𝑋 )
19 eqcom ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑋 ) ↔ ( 𝐺 ‘ 𝑋 ) = 𝑧 )
20 fnbrfvb ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑋 ) = 𝑧 ↔ 𝑋 𝐺 𝑧 ) )
21 19 20 syl5bb ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 = ( 𝐺 ‘ 𝑋 ) ↔ 𝑋 𝐺 𝑧 ) )
22 21 biimpd ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 = ( 𝐺 ‘ 𝑋 ) → 𝑋 𝐺 𝑧 ) )
23 breq1 ⊢ ( ( 𝐺 ‘ 𝑋 ) = 𝑧 → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ↔ 𝑧 𝐹 𝑦 ) )
24 23 eqcoms ⊢ ( 𝑧 = ( 𝐺 ‘ 𝑋 ) → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ↔ 𝑧 𝐹 𝑦 ) )
25 24 biimpcd ⊢ ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 → ( 𝑧 = ( 𝐺 ‘ 𝑋 ) → 𝑧 𝐹 𝑦 ) )
26 22 25 anim12ii ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → ( 𝑧 = ( 𝐺 ‘ 𝑋 ) → ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) ) )
27 26 eximdv ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → ( ∃ 𝑧 𝑧 = ( 𝐺 ‘ 𝑋 ) → ∃ 𝑧 ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) ) )
28 18 27 mpi ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → ∃ 𝑧 ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) )
29 simpr ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
30 vex ⊢ 𝑦 ∈ V
31 brcog ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑦 ∈ V ) → ( 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ↔ ∃ 𝑧 ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) ) )
32 29 30 31 sylancl ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ↔ ∃ 𝑧 ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) ) )
33 32 adantr ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → ( 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ↔ ∃ 𝑧 ( 𝑋 𝐺 𝑧 ∧ 𝑧 𝐹 𝑦 ) ) )
34 28 33 mpbird ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 )
35 30 brresi ⊢ ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ ( 𝑋 ∈ { 𝑋 } ∧ 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) )
36 snidg ⊢ ( 𝑋 ∈ 𝐴 → 𝑋 ∈ { 𝑋 } )
37 36 biantrurd ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ↔ ( 𝑋 ∈ { 𝑋 } ∧ 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) ) )
38 35 37 bitr4id ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) )
39 38 ad2antlr ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ 𝑋 ( 𝐹 ∘ 𝐺 ) 𝑦 ) )
40 34 39 mpbird ⊢ ( ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) → 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 )
41 40 ex ⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 → 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
42 41 adantl ⊢ ( ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 → 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
43 breq1 ⊢ ( 𝑋 = 𝑥 → ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
44 43 eqcoms ⊢ ( 𝑥 = 𝑋 → ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
45 44 ad2antlr ⊢ ( ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑋 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ↔ 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
46 42 45 sylibd ⊢ ( ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 → 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 ) )
47 46 moimdv ⊢ ( ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) )
48 47 ex ⊢ ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
49 48 com23 ⊢ ( ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) ∧ 𝑥 = 𝑋 ) → ( ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
50 16 49 rspcimdv ⊢ ( ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } ∧ 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ) → ( ∀ 𝑥 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
51 50 ex ⊢ ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( ∀ 𝑥 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) ) )
52 51 com13 ⊢ ( ∀ 𝑥 ∈ dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ∃* 𝑦 𝑥 ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) 𝑦 → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) ) )
53 10 52 simplbiim ⊢ ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) ) )
54 53 com13 ⊢ ( dom ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) = { 𝑋 } → ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) ) )
55 9 54 mpcom ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
56 55 imp31 ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 )
57 17 snid ⊢ ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) }
58 57 biantrur ⊢ ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) )
59 58 a1i ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
60 59 mobidv ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ∃* 𝑦 ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ↔ ∃* 𝑦 ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ) )
61 56 60 mpbid ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∃* 𝑦 ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) )
62 61 adantl ⊢ ( ( 𝑥 = ( 𝐺 ‘ 𝑋 ) ∧ ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) ) → ∃* 𝑦 ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) )
63 breq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ↔ ( 𝐺 ‘ 𝑋 ) ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
64 30 brresi ⊢ ( ( 𝐺 ‘ 𝑋 ) ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ↔ ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) )
65 63 64 bitr2di ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ↔ 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
66 65 adantr ⊢ ( ( 𝑥 = ( 𝐺 ‘ 𝑋 ) ∧ ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) ) → ( ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ↔ 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
67 66 mobidv ⊢ ( ( 𝑥 = ( 𝐺 ‘ 𝑋 ) ∧ ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) ) → ( ∃* 𝑦 ( ( 𝐺 ‘ 𝑋 ) ∈ { ( 𝐺 ‘ 𝑋 ) } ∧ ( 𝐺 ‘ 𝑋 ) 𝐹 𝑦 ) ↔ ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
68 62 67 mpbid ⊢ ( ( 𝑥 = ( 𝐺 ‘ 𝑋 ) ∧ ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 )
69 68 ex ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
70 8 69 sylbi ⊢ ( 𝑥 ∈ { ( 𝐺 ‘ 𝑋 ) } → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
71 7 70 syl6bi ⊢ ( dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) )
72 71 com23 ⊢ ( dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) = { ( 𝐺 ‘ 𝑋 ) } → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) )
73 6 72 syl ⊢ ( ( 𝐺 ‘ 𝑋 ) ∈ dom 𝐹 → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) )
74 5 73 syl6com ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) ) )
75 74 a1d ⊢ ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) → ( Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) → ( ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) ) ) )
76 75 imp31 ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) ) )
77 76 pm2.43i ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) → ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
78 77 ralrimiv ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 )
79 dffun7 ⊢ ( Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ↔ ( Rel ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) ∃* 𝑦 𝑥 ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) 𝑦 ) )
80 2 78 79 sylanbrc ⊢ ( ( ( 𝑋 ∈ dom ( 𝐹 ∘ 𝐺 ) ∧ Fun ( ( 𝐹 ∘ 𝐺 ) ↾ { 𝑋 } ) ) ∧ ( 𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → Fun ( 𝐹 ↾ { ( 𝐺 ‘ 𝑋 ) } ) )