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 42816
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 5770 . . 3 Rel (𝐹 ↾ {(𝐺𝑋)})
21a1i 11 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Rel (𝐹 ↾ {(𝐺𝑋)}))
3 dmfco 6631 . . . . . . . . 9 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) ↔ (𝐺𝑋) ∈ dom 𝐹))
43biimpd 230 . . . . . . . 8 ((Fun 𝐺𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
54funfni 6334 . . . . . . 7 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋 ∈ dom (𝐹𝐺) → (𝐺𝑋) ∈ dom 𝐹))
6 dmressnsn 5782 . . . . . . . 8 ((𝐺𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)})
7 eleq2 2873 . . . . . . . . . 10 (dom (𝐹 ↾ {(𝐺𝑋)}) = {(𝐺𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) ↔ 𝑥 ∈ {(𝐺𝑋)}))
8 velsn 4494 . . . . . . . . . . 11 (𝑥 ∈ {(𝐺𝑋)} ↔ 𝑥 = (𝐺𝑋))
9 dmressnsn 5782 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ dom (𝐹𝐺) → dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋})
10 dffun7 6259 . . . . . . . . . . . . . . . . . . 19 (Fun ((𝐹𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
11 snidg 4510 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑋 ∈ dom (𝐹𝐺) → 𝑋 ∈ {𝑋})
1211adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ {𝑋})
13 eleq2 2873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ({𝑋} = dom ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1413eqcoms 2805 . . . . . . . . . . . . . . . . . . . . . . . 24 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1514adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋})))
1612, 15mpbid 233 . . . . . . . . . . . . . . . . . . . . . 22 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → 𝑋 ∈ dom ((𝐹𝐺) ↾ {𝑋}))
17 fvex 6558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝐺𝑋) ∈ V
1817isseti 3454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 𝑧 𝑧 = (𝐺𝑋)
19 eqcom 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (𝑧 = (𝐺𝑋) ↔ (𝐺𝑋) = 𝑧)
20 fnbrfvb 6593 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋) = 𝑧𝑋𝐺𝑧))
2119, 20syl5bb 284 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) ↔ 𝑋𝐺𝑧))
2221biimpd 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑧 = (𝐺𝑋) → 𝑋𝐺𝑧))
23 breq1 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((𝐺𝑋) = 𝑧 → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2423eqcoms 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (𝑧 = (𝐺𝑋) → ((𝐺𝑋)𝐹𝑦𝑧𝐹𝑦))
2524biimpcd 250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐺𝑋)𝐹𝑦 → (𝑧 = (𝐺𝑋) → 𝑧𝐹𝑦))
2622, 25anim12ii 617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑧 = (𝐺𝑋) → (𝑋𝐺𝑧𝑧𝐹𝑦)))
2726eximdv 1899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺𝑋) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
2818, 27mpi 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦))
29 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝐺 Fn 𝐴𝑋𝐴) → 𝑋𝐴)
30 vex 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 𝑦 ∈ V
31 brcog 5630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((𝑋𝐴𝑦 ∈ V) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3229, 30, 31sylancl 586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((𝐺 Fn 𝐴𝑋𝐴) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3332adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋(𝐹𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧𝑧𝐹𝑦)))
3428, 33mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋(𝐹𝐺)𝑦)
35 snidg 4510 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑋𝐴𝑋 ∈ {𝑋})
3635biantrurd 533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋𝐴 → (𝑋(𝐹𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦)))
3730brresi 5750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑋((𝐹𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹𝐺)𝑦))
3836, 37syl6rbbr 291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑋𝐴 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
3938ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑋(𝐹𝐺)𝑦))
4034, 39mpbird 258 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝐺 Fn 𝐴𝑋𝐴) ∧ (𝐺𝑋)𝐹𝑦) → 𝑋((𝐹𝐺) ↾ {𝑋})𝑦)
4140ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐺 Fn 𝐴𝑋𝐴) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
4241adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑋((𝐹𝐺) ↾ {𝑋})𝑦))
43 breq1 4971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑋 = 𝑥 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4443eqcoms 2805 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = 𝑋 → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4544ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑋((𝐹𝐺) ↾ {𝑋})𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4642, 45sylibd 240 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦𝑥((𝐹𝐺) ↾ {𝑋})𝑦))
4746moimdv 2585 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦))
4847ex 413 . . . . . . . . . . . . . . . . . . . . . . 23 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴𝑋𝐴) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
4948com23 86 . . . . . . . . . . . . . . . . . . . . . 22 (((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5016, 49rspcimdv 3562 . . . . . . . . . . . . . . . . . . . . 21 ((dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹𝐺)) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5150ex 413 . . . . . . . . . . . . . . . . . . . 20 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5251com13 88 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ dom ((𝐹𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5310, 52simplbiim 505 . . . . . . . . . . . . . . . . . 18 (Fun ((𝐹𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹𝐺) → (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
5453com13 88 . . . . . . . . . . . . . . . . 17 (dom ((𝐹𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦))))
559, 54mpcom 38 . . . . . . . . . . . . . . . 16 (𝑋 ∈ dom (𝐹𝐺) → (Fun ((𝐹𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴𝑋𝐴) → ∃*𝑦(𝐺𝑋)𝐹𝑦)))
5655imp31 418 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦(𝐺𝑋)𝐹𝑦)
5717snid 4512 . . . . . . . . . . . . . . . . . 18 (𝐺𝑋) ∈ {(𝐺𝑋)}
5857biantrur 531 . . . . . . . . . . . . . . . . 17 ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
5958a1i 11 . . . . . . . . . . . . . . . 16 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ((𝐺𝑋)𝐹𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6059mobidv 2590 . . . . . . . . . . . . . . 15 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (∃*𝑦(𝐺𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦)))
6156, 60mpbid 233 . . . . . . . . . . . . . 14 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6261adantl 482 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
63 breq1 4971 . . . . . . . . . . . . . . . 16 (𝑥 = (𝐺𝑋) → (𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ (𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦))
6430brresi 5750 . . . . . . . . . . . . . . . 16 ((𝐺𝑋)(𝐹 ↾ {(𝐺𝑋)})𝑦 ↔ ((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦))
6563, 64syl6rbb 289 . . . . . . . . . . . . . . 15 (𝑥 = (𝐺𝑋) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6665adantr 481 . . . . . . . . . . . . . 14 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6766mobidv 2590 . . . . . . . . . . . . 13 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → (∃*𝑦((𝐺𝑋) ∈ {(𝐺𝑋)} ∧ (𝐺𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
6862, 67mpbid 233 . . . . . . . . . . . 12 ((𝑥 = (𝐺𝑋) ∧ ((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
6968ex 413 . . . . . . . . . . 11 (𝑥 = (𝐺𝑋) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
708, 69sylbi 218 . . . . . . . . . 10 (𝑥 ∈ {(𝐺𝑋)} → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
717, 70syl6bi 254 . . . . . . . . 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 418 . . . 4 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)))
7776pm2.43i 52 . . 3 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
7877ralrimiv 3150 . 2 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦)
79 dffun7 6259 . 2 (Fun (𝐹 ↾ {(𝐺𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺𝑋)})𝑦))
802, 78, 79sylanbrc 583 1 (((𝑋 ∈ dom (𝐹𝐺) ∧ Fun ((𝐹𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴𝑋𝐴)) → Fun (𝐹 ↾ {(𝐺𝑋)}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1525  wex 1765  wcel 2083  ∃*wmo 2576  wral 3107  Vcvv 3440  {csn 4478   class class class wbr 4968  dom cdm 5450  cres 5452  ccom 5454  Rel wrel 5455  Fun wfun 6226   Fn wfn 6227  cfv 6232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-res 5462  df-iota 6196  df-fun 6234  df-fn 6235  df-fv 6240
This theorem is referenced by:  afvco2  42913
  Copyright terms: Public domain W3C validator