Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  funressnfv Structured version   Visualization version   GIF version

Theorem funressnfv 40512
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.)
Assertion
Ref Expression
funressnfv (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))

Proof of Theorem funressnfv
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relres 5385 . . 3 Rel (𝐹 ↾ {(𝐺𝑋)})
21a1i 11 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Rel (𝐹 ↾ {(𝐺𝑋)}))
3 dmfco 6229 . . . . . . . . 9 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) ↔ (𝐺𝑋) ∈ dom 𝐹))
43biimpd 219 . . . . . . . 8 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
54funfni 5949 . . . . . . 7 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
6 dmressnsn 5397 . . . . . . . 8 ((𝐺𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)})
7 eleq2 2687 . . . . . . . . . 10 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) ↔ 𝑥 ∈ {(𝐺𝑋)}))
8 velsn 4164 . . . . . . . . . . 11 (𝑥 ∈ {(𝐺𝑋)} ↔ 𝑥 = (𝐺𝑋))
9 dmressnsn 5397 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ dom (𝐹𝐺) → dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋})
10 dffun7 5874 . . . . . . . . . . . . . . . . . . 19 (Fun ((𝐹𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
11 snidg 4177 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋 ∈ dom (𝐹𝐺) → 𝑋 ∈ {𝑋})
1211adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ {𝑋})
13 eleq2 2687 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({𝑋} = dom ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1413eqcoms 2629 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1514adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1612, 15mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋}))
17 fvex 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑋) ∈ V
1817isseti 3195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑧 𝑧 = (𝐺𝑋)
19 eqcom 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 = (𝐺𝑋) ↔ (𝐺𝑋) = 𝑧)
20 fnbrfvb 6193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋) = 𝑧𝑋𝐺𝑧))
2119, 20syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) ↔ 𝑋𝐺𝑧))
2221biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) → 𝑋𝐺𝑧))
23 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐺𝑋) = 𝑧 → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2423eqcoms 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = (𝐺𝑋) → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2524biimpcd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺𝑋)𝐹𝑦 → (𝑧 = (𝐺𝑋) → 𝑧𝐹𝑦))
2622, 25anim12ii 593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑧 = (𝐺𝑋) → (𝑋𝐺𝑧𝑧𝐹𝑦)))
2726eximdv 1843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺𝑋) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
2818, 27mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦))
29 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐺 Fn 𝐴𝑋𝐴) → 𝑋𝐴)
30 vex 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑦 ∈ V
31 brcog 5248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑋𝐴𝑦 ∈ V) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3229, 30, 31sylancl 693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3332adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3428, 33mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋(𝐹𝐺)𝑦)
35 snidg 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑋𝐴𝑋 ∈ {𝑋})
3635biantrud 528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋𝐴 → (𝑋(𝐹𝐺)𝑦 ↔ (𝑋(𝐹𝐺)𝑦𝑋 ∈ {𝑋})))
3730brres 5362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋((𝐹𝐺) ↾ {𝑋})𝑦 ↔ (𝑋(𝐹𝐺)𝑦𝑋 ∈ {𝑋}))
3836, 37syl6rbbr 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋𝐴 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
3938ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
4034, 39mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋((𝐹𝐺) ↾ {𝑋})𝑦)
4140ex 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
4241adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
43 breq1 4616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋 = 𝑥 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4443eqcoms 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑋 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4544ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4642, 45sylibd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4746alrimiv 1852 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑦((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
48 moim 2518 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑦((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
4947, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
5049ex 450 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴𝑋𝐴) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5150com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5216, 51rspcimdv 3296 . . . . . . . . . . . . . . . . . . . . . 22 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5352ex 450 . . . . . . . . . . . . . . . . . . . . 21 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5453com13 88 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5554adantl 482 . . . . . . . . . . . . . . . . . . 19 ((Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦) → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5610, 55sylbi 207 . . . . . . . . . . . . . . . . . 18 (Fun ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5756com13 88 . . . . . . . . . . . . . . . . 17 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
589, 57mpcom 38 . . . . . . . . . . . . . . . 16 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5958imp31 448 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦(𝐺𝑋)𝐹𝑦)
6017snid 4179 . . . . . . . . . . . . . . . . . 18 (𝐺𝑋) ∈ {(𝐺𝑋)}
6160biantru 526 . . . . . . . . . . . . . . . . 17 ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6261a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)})))
6362mobidv 2490 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦(𝐺𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)})))
6459, 63mpbid 222 . . . . . . . . . . . . . 14 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6564adantl 482 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
66 breq1 4616 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐺𝑋) → (𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ (𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦))
6730brres 5362 . . . . . . . . . . . . . . . 16 ((𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6866, 67syl6rbb 277 . . . . . . . . . . . . . . 15 (𝑥 = (𝐺𝑋) → (((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6968adantr 481 . . . . . . . . . . . . . 14 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7069mobidv 2490 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7165, 70mpbid 222 . . . . . . . . . . . 12 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
7271ex 450 . . . . . . . . . . 11 (𝑥 = (𝐺𝑋) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
738, 72sylbi 207 . . . . . . . . . 10 (𝑥 ∈ {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
747, 73syl6bi 243 . . . . . . . . 9 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
7574com23 86 . . . . . . . 8 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
766, 75syl 17 . . . . . . 7 ((𝐺𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
775, 76syl6com 37 . . . . . 6 (𝑋 ∈ dom (𝐹𝐺) → ((𝐺 Fn 𝐴𝑋𝐴) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))))
7877a1d 25 . . . . 5 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))))
7978imp31 448 . . . 4 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
8079pm2.43i 52 . . 3 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
8180ralrimiv 2959 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
82 dffun7 5874 . 2 (Fun (𝐹 ↾ {(𝐺𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
832, 81, 82sylanbrc 697 1 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  ∃*wmo 2470  wral 2907  Vcvv 3186  {csn 4148   class class class wbr 4613  dom cdm 5074  cres 5076  ccom 5078  Rel wrel 5079  Fun wfun 5841   Fn wfn 5842  cfv 5847
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-res 5086  df-iota 5810  df-fun 5849  df-fn 5850  df-fv 5855
This theorem is referenced by:  afvco2  40560
  Copyright terms: Public domain W3C validator