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 46051
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.)
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 6009 . . 3 Rel (𝐹 ↾ {(𝐺𝑋)})
21a1i 11 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Rel (𝐹 ↾ {(𝐺𝑋)}))
3 dmfco 6986 . . . . . . . . 9 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) ↔ (𝐺𝑋) ∈ dom 𝐹))
43biimpd 228 . . . . . . . 8 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
54funfni 6654 . . . . . . 7 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
6 dmressnsn 6022 . . . . . . . 8 ((𝐺𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)})
7 eleq2 2820 . . . . . . . . . 10 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) ↔ 𝑥 ∈ {(𝐺𝑋)}))
8 velsn 4643 . . . . . . . . . . 11 (𝑥 ∈ {(𝐺𝑋)} ↔ 𝑥 = (𝐺𝑋))
9 dmressnsn 6022 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ dom (𝐹𝐺) → dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋})
10 dffun7 6574 . . . . . . . . . . . . . . . . . . 19 (Fun ((𝐹𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
11 snidg 4661 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ dom (𝐹𝐺) → 𝑋 ∈ {𝑋})
1211adantl 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ {𝑋})
13 eleq2 2820 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑋} = dom ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1413eqcoms 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1514adantr 479 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1612, 15mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋}))
17 fvex 6903 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐺𝑋) ∈ V
1817isseti 3488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 𝑧 = (𝐺𝑋)
19 eqcom 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝐺𝑋) ↔ (𝐺𝑋) = 𝑧)
20 fnbrfvb 6943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋) = 𝑧𝑋𝐺𝑧))
2119, 20bitrid 282 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) ↔ 𝑋𝐺𝑧))
2221biimpd 228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) → 𝑋𝐺𝑧))
23 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺𝑋) = 𝑧 → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2423eqcoms 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝐺𝑋) → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2524biimpcd 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑋)𝐹𝑦 → (𝑧 = (𝐺𝑋) → 𝑧𝐹𝑦))
2622, 25anim12ii 616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑧 = (𝐺𝑋) → (𝑋𝐺𝑧𝑧𝐹𝑦)))
2726eximdv 1918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺𝑋) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
2818, 27mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦))
29 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐺 Fn 𝐴𝑋𝐴) → 𝑋𝐴)
30 vex 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑦 ∈ V
31 brcog 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑋𝐴𝑦 ∈ V) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3229, 30, 31sylancl 584 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3332adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3428, 33mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋(𝐹𝐺)𝑦)
3530brresi 5989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋((𝐹𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦))
36 snidg 4661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋𝐴𝑋 ∈ {𝑋})
3736biantrurd 531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋𝐴 → (𝑋(𝐹𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦)))
3835, 37bitr4id 289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋𝐴 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
3938ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
4034, 39mpbird 256 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋((𝐹𝐺) ↾ {𝑋})𝑦)
4140ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
4241adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
43 breq1 5150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 = 𝑥 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4443eqcoms 2738 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑋 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4544ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4642, 45sylibd 238 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4746moimdv 2538 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
4847ex 411 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴𝑋𝐴) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
4948com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5016, 49rspcimdv 3601 . . . . . . . . . . . . . . . . . . . . 21 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5150ex 411 . . . . . . . . . . . . . . . . . . . 20 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5251com13 88 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5310, 52simplbiim 503 . . . . . . . . . . . . . . . . . 18 (Fun ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5453com13 88 . . . . . . . . . . . . . . . . 17 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
559, 54mpcom 38 . . . . . . . . . . . . . . . 16 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5655imp31 416 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦(𝐺𝑋)𝐹𝑦)
5717snid 4663 . . . . . . . . . . . . . . . . . 18 (𝐺𝑋) ∈ {(𝐺𝑋)}
5857biantrur 529 . . . . . . . . . . . . . . . . 17 ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
5958a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6059mobidv 2541 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦(𝐺𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6156, 60mpbid 231 . . . . . . . . . . . . . 14 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6261adantl 480 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
63 breq1 5150 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐺𝑋) → (𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ (𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦))
6430brresi 5989 . . . . . . . . . . . . . . . 16 ((𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6563, 64bitr2di 287 . . . . . . . . . . . . . . 15 (𝑥 = (𝐺𝑋) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6665adantr 479 . . . . . . . . . . . . . 14 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6766mobidv 2541 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6862, 67mpbid 231 . . . . . . . . . . . 12 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
6968ex 411 . . . . . . . . . . 11 (𝑥 = (𝐺𝑋) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
708, 69sylbi 216 . . . . . . . . . 10 (𝑥 ∈ {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
717, 70syl6bi 252 . . . . . . . . 9 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
7271com23 86 . . . . . . . 8 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
736, 72syl 17 . . . . . . 7 ((𝐺𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
745, 73syl6com 37 . . . . . 6 (𝑋 ∈ dom (𝐹𝐺) → ((𝐺 Fn 𝐴𝑋𝐴) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))))
7574a1d 25 . . . . 5 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))))
7675imp31 416 . . . 4 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
7776pm2.43i 52 . . 3 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7877ralrimiv 3143 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
79 dffun7 6574 . 2 (Fun (𝐹 ↾ {(𝐺𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
802, 78, 79sylanbrc 581 1 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1539  wex 1779  wcel 2104  ∃*wmo 2530  wral 3059  Vcvv 3472  {csn 4627   class class class wbr 5147  dom cdm 5675  cres 5677  ccom 5679  Rel wrel 5680  Fun wfun 6536   Fn wfn 6537  cfv 6542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-res 5687  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550
This theorem is referenced by:  afvco2  46182
  Copyright terms: Public domain W3C validator