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 47055
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 6023 . . 3 Rel (𝐹 ↾ {(𝐺𝑋)})
21a1i 11 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Rel (𝐹 ↾ {(𝐺𝑋)}))
3 dmfco 7005 . . . . . . . . 9 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) ↔ (𝐺𝑋) ∈ dom 𝐹))
43biimpd 229 . . . . . . . 8 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
54funfni 6674 . . . . . . 7 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
6 dmressnsn 6041 . . . . . . . 8 ((𝐺𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)})
7 eleq2 2830 . . . . . . . . . 10 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) ↔ 𝑥 ∈ {(𝐺𝑋)}))
8 velsn 4642 . . . . . . . . . . 11 (𝑥 ∈ {(𝐺𝑋)} ↔ 𝑥 = (𝐺𝑋))
9 dmressnsn 6041 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ dom (𝐹𝐺) → dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋})
10 dffun7 6593 . . . . . . . . . . . . . . . . . . 19 (Fun ((𝐹𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
11 snidg 4660 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ dom (𝐹𝐺) → 𝑋 ∈ {𝑋})
1211adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ {𝑋})
13 eleq2 2830 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑋} = dom ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1413eqcoms 2745 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1514adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1612, 15mpbid 232 . . . . . . . . . . . . . . . . . . . . . 22 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋}))
17 fvex 6919 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐺𝑋) ∈ V
1817isseti 3498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 𝑧 = (𝐺𝑋)
19 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝐺𝑋) ↔ (𝐺𝑋) = 𝑧)
20 fnbrfvb 6959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋) = 𝑧𝑋𝐺𝑧))
2119, 20bitrid 283 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) ↔ 𝑋𝐺𝑧))
2221biimpd 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) → 𝑋𝐺𝑧))
23 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺𝑋) = 𝑧 → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2423eqcoms 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝐺𝑋) → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2524biimpcd 249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑋)𝐹𝑦 → (𝑧 = (𝐺𝑋) → 𝑧𝐹𝑦))
2622, 25anim12ii 618 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑧 = (𝐺𝑋) → (𝑋𝐺𝑧𝑧𝐹𝑦)))
2726eximdv 1917 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺𝑋) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
2818, 27mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦))
29 simpr 484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐺 Fn 𝐴𝑋𝐴) → 𝑋𝐴)
30 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑦 ∈ V
31 brcog 5877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑋𝐴𝑦 ∈ V) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3229, 30, 31sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3332adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3428, 33mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋(𝐹𝐺)𝑦)
3530brresi 6006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋((𝐹𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦))
36 snidg 4660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋𝐴𝑋 ∈ {𝑋})
3736biantrurd 532 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋𝐴 → (𝑋(𝐹𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦)))
3835, 37bitr4id 290 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋𝐴 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
3938ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
4034, 39mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋((𝐹𝐺) ↾ {𝑋})𝑦)
4140ex 412 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
4241adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
43 breq1 5146 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 = 𝑥 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4443eqcoms 2745 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑋 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4544ad2antlr 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4642, 45sylibd 239 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4746moimdv 2546 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
4847ex 412 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴𝑋𝐴) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
4948com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5016, 49rspcimdv 3612 . . . . . . . . . . . . . . . . . . . . 21 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5150ex 412 . . . . . . . . . . . . . . . . . . . 20 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5251com13 88 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5310, 52simplbiim 504 . . . . . . . . . . . . . . . . . 18 (Fun ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5453com13 88 . . . . . . . . . . . . . . . . 17 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
559, 54mpcom 38 . . . . . . . . . . . . . . . 16 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5655imp31 417 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦(𝐺𝑋)𝐹𝑦)
5717snid 4662 . . . . . . . . . . . . . . . . . 18 (𝐺𝑋) ∈ {(𝐺𝑋)}
5857biantrur 530 . . . . . . . . . . . . . . . . 17 ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
5958a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6059mobidv 2549 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦(𝐺𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6156, 60mpbid 232 . . . . . . . . . . . . . 14 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6261adantl 481 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
63 breq1 5146 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐺𝑋) → (𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ (𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦))
6430brresi 6006 . . . . . . . . . . . . . . . 16 ((𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6563, 64bitr2di 288 . . . . . . . . . . . . . . 15 (𝑥 = (𝐺𝑋) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6665adantr 480 . . . . . . . . . . . . . 14 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6766mobidv 2549 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6862, 67mpbid 232 . . . . . . . . . . . 12 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
6968ex 412 . . . . . . . . . . 11 (𝑥 = (𝐺𝑋) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
708, 69sylbi 217 . . . . . . . . . 10 (𝑥 ∈ {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
717, 70biimtrdi 253 . . . . . . . . 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 417 . . . 4 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
7776pm2.43i 52 . . 3 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7877ralrimiv 3145 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
79 dffun7 6593 . 2 (Fun (𝐹 ↾ {(𝐺𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
802, 78, 79sylanbrc 583 1 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  ∃*wmo 2538  wral 3061  Vcvv 3480  {csn 4626   class class class wbr 5143  dom cdm 5685  cres 5687  ccom 5689  Rel wrel 5690  Fun wfun 6555   Fn wfn 6556  cfv 6561
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-res 5697  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569
This theorem is referenced by:  afvco2  47188
  Copyright terms: Public domain W3C validator