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 41714
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 5584 . . 3 Rel (𝐹 ↾ {(𝐺𝑋)})
21a1i 11 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Rel (𝐹 ↾ {(𝐺𝑋)}))
3 dmfco 6434 . . . . . . . . 9 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) ↔ (𝐺𝑋) ∈ dom 𝐹))
43biimpd 219 . . . . . . . 8 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
54funfni 6152 . . . . . . 7 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
6 dmressnsn 5596 . . . . . . . 8 ((𝐺𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)})
7 eleq2 2828 . . . . . . . . . 10 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) ↔ 𝑥 ∈ {(𝐺𝑋)}))
8 velsn 4337 . . . . . . . . . . 11 (𝑥 ∈ {(𝐺𝑋)} ↔ 𝑥 = (𝐺𝑋))
9 dmressnsn 5596 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ dom (𝐹𝐺) → dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋})
10 dffun7 6076 . . . . . . . . . . . . . . . . . . 19 (Fun ((𝐹𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
11 snidg 4351 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑋 ∈ dom (𝐹𝐺) → 𝑋 ∈ {𝑋})
1211adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ {𝑋})
13 eleq2 2828 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ({𝑋} = dom ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1413eqcoms 2768 . . . . . . . . . . . . . . . . . . . . . . . . 25 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1514adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1612, 15mpbid 222 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋}))
17 fvex 6362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝐺𝑋) ∈ V
1817isseti 3349 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 𝑧 𝑧 = (𝐺𝑋)
19 eqcom 2767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (𝑧 = (𝐺𝑋) ↔ (𝐺𝑋) = 𝑧)
20 fnbrfvb 6397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋) = 𝑧𝑋𝐺𝑧))
2119, 20syl5bb 272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) ↔ 𝑋𝐺𝑧))
2221biimpd 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) → 𝑋𝐺𝑧))
23 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐺𝑋) = 𝑧 → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2423eqcoms 2768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 (𝑧 = (𝐺𝑋) → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2524biimpcd 239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺𝑋)𝐹𝑦 → (𝑧 = (𝐺𝑋) → 𝑧𝐹𝑦))
2622, 25anim12ii 595 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑧 = (𝐺𝑋) → (𝑋𝐺𝑧𝑧𝐹𝑦)))
2726eximdv 1995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺𝑋) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
2818, 27mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦))
29 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐺 Fn 𝐴𝑋𝐴) → 𝑋𝐴)
30 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 𝑦 ∈ V
31 brcog 5444 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝑋𝐴𝑦 ∈ V) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3229, 30, 31sylancl 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3332adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3428, 33mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋(𝐹𝐺)𝑦)
35 snidg 4351 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑋𝐴𝑋 ∈ {𝑋})
3635biantrud 529 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋𝐴 → (𝑋(𝐹𝐺)𝑦 ↔ (𝑋(𝐹𝐺)𝑦𝑋 ∈ {𝑋})))
3730brres 5560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (𝑋((𝐹𝐺) ↾ {𝑋})𝑦 ↔ (𝑋(𝐹𝐺)𝑦𝑋 ∈ {𝑋}))
3836, 37syl6rbbr 279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋𝐴 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
3938ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
4034, 39mpbird 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋((𝐹𝐺) ↾ {𝑋})𝑦)
4140ex 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
4241adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
43 breq1 4807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋 = 𝑥 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4443eqcoms 2768 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑥 = 𝑋 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4544ad2antlr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4642, 45sylibd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4746alrimiv 2004 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑦((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
48 moim 2657 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (∀𝑦((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
4947, 48syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
5049ex 449 . . . . . . . . . . . . . . . . . . . . . . . 24 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴𝑋𝐴) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5150com23 86 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5216, 51rspcimdv 3450 . . . . . . . . . . . . . . . . . . . . . 22 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5352ex 449 . . . . . . . . . . . . . . . . . . . . 21 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5453com13 88 . . . . . . . . . . . . . . . . . . . 20 (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5554adantl 473 . . . . . . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦(𝐺𝑋)𝐹𝑦)
6017snid 4353 . . . . . . . . . . . . . . . . . 18 (𝐺𝑋) ∈ {(𝐺𝑋)}
6160biantru 527 . . . . . . . . . . . . . . . . 17 ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6261a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)})))
6362mobidv 2628 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦(𝐺𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)})))
6459, 63mpbid 222 . . . . . . . . . . . . . 14 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6564adantl 473 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
66 breq1 4807 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐺𝑋) → (𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ (𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦))
6730brres 5560 . . . . . . . . . . . . . . . 16 ((𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ ((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}))
6866, 67syl6rbb 277 . . . . . . . . . . . . . . 15 (𝑥 = (𝐺𝑋) → (((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6968adantr 472 . . . . . . . . . . . . . 14 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7069mobidv 2628 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (∃*𝑦((𝐺𝑋)𝐹𝑦 ∧ (𝐺𝑋) ∈ {(𝐺𝑋)}) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7165, 70mpbid 222 . . . . . . . . . . . 12 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
7271ex 449 . . . . . . . . . . 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 447 . . . 4 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
8079pm2.43i 52 . . 3 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
8180ralrimiv 3103 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
82 dffun7 6076 . 2 (Fun (𝐹 ↾ {(𝐺𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
832, 81, 82sylanbrc 701 1 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1630   = wceq 1632  wex 1853  wcel 2139  ∃*wmo 2608  wral 3050  Vcvv 3340  {csn 4321   class class class wbr 4804  dom cdm 5266  cres 5268  ccom 5270  Rel wrel 5271  Fun wfun 6043   Fn wfn 6044  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-res 5278  df-iota 6012  df-fun 6051  df-fn 6052  df-fv 6057
This theorem is referenced by:  afvco2  41762
  Copyright terms: Public domain W3C validator