Theorem funressnfv 47037

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.

Step	Hyp	Ref	Expression
1		relres 5965	. . 3 ⊢ Rel (𝐹 ↾ {(𝐺‘𝑋)})
2	1	a1i 11	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Rel (𝐹 ↾ {(𝐺‘𝑋)}))
3		dmfco 6939	. . . . . . . . 9 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹))
4	3	biimpd 229	. . . . . . . 8 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
5	4	funfni 6606	. . . . . . 7 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
6		dmressnsn 5983	. . . . . . . 8 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)})
7		eleq2 2817	. . . . . . . . . 10 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) ↔ 𝑥 ∈ {(𝐺‘𝑋)}))
8		velsn 4601	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} ↔ 𝑥 = (𝐺‘𝑋))
9		dmressnsn 5983	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋})
10		dffun7 6527	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
11		snidg 4620	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → 𝑋 ∈ {𝑋})
12	11	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ {𝑋})
13		eleq2 2817	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({𝑋} = dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
14	13	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
15	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
16	12, 15	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))
17		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐺‘𝑋) ∈ V
18	17	isseti 3462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∃𝑧 𝑧 = (𝐺‘𝑋)
19		eqcom 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝐺‘𝑋) ↔ (𝐺‘𝑋) = 𝑧)
20		fnbrfvb 6893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) = 𝑧 ↔ 𝑋𝐺𝑧))
21	19, 20	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) ↔ 𝑋𝐺𝑧))
22	21	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) → 𝑋𝐺𝑧))
23		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘𝑋) = 𝑧 → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
24	23	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝐺‘𝑋) → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
25	24	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑋)𝐹𝑦 → (𝑧 = (𝐺‘𝑋) → 𝑧𝐹𝑦))
26	22, 25	anim12ii 618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑧 = (𝐺‘𝑋) → (𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
27	26	eximdv 1917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺‘𝑋) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
28	18, 27	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))
29		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
30		vex 3448	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑦 ∈ V
31		brcog 5820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
32	29, 30, 31	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
33	32	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
34	28, 33	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋(𝐹 ∘ 𝐺)𝑦)
35	30	brresi 5948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦))
36		snidg 4620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ {𝑋})
37	36	biantrurd 532	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋 ∈ 𝐴 → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦)))
38	35, 37	bitr4id 290	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 ∈ 𝐴 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
39	38	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
40	34, 39	mpbird 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)
41	40	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
42	41	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
43		breq1 5105	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 = 𝑥 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
44	43	eqcoms 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑋 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
45	44	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
46	42, 45	sylibd 239	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
47	46	moimdv 2539	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))
48	47	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
49	48	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
50	16, 49	rspcimdv 3575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
51	50	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
52	51	com13 88	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
53	10, 52	simplbiim 504	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
54	53	com13 88	. . . . . . . . . . . . . . . . 17 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
55	9, 54	mpcom 38	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
56	55	imp31 417	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)
57	17	snid 4622	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}
58	57	biantrur 530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
59	58	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
60	59	mobidv 2542	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦(𝐺‘𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
61	56, 60	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
62	61	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
63		breq1 5105	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐺‘𝑋) → (𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ (𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
64	30	brresi 5948	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
65	63, 64	bitr2di 288	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
66	65	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
67	66	mobidv 2542	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
68	62, 67	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
69	68	ex 412	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
70	8, 69	sylbi 217	. . . . . . . . . 10 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
71	7, 70	biimtrdi 253	. . . . . . . . 9 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
72	71	com23 86	. . . . . . . 8 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
73	6, 72	syl 17	. . . . . . 7 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
74	5, 73	syl6com 37	. . . . . 6 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))))
75	74	a1d 25	. . . . 5 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))))
76	75	imp31 417	. . . 4 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
77	76	pm2.43i 52	. . 3 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
78	77	ralrimiv 3124	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
79		dffun7 6527	. 2 ⊢ (Fun (𝐹 ↾ {(𝐺‘𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺‘𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
80	2, 78, 79	sylanbrc 583	1 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃*wmo 2531  ∀wral 3044  Vcvv 3444  {csn 4585   class class class wbr 5102  dom cdm 5631   ↾ cres 5633   ∘ ccom 5635  Rel wrel 5636  Fun wfun 6493   Fn wfn 6494  ‘cfv 6499

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-res 5643  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  afvco2  47170