Theorem funressnfv 47704

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 6005	. . 3 ⊢ Rel (𝐹 ↾ {(𝐺‘𝑋)})
2	1	a1i 11	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Rel (𝐹 ↾ {(𝐺‘𝑋)}))
3		dmfco 6978	. . . . . . . . 9 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹))
4	3	biimpd 232	. . . . . . . 8 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
5	4	funfni 6642	. . . . . . 7 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
6		dmressnsn 6023	. . . . . . . 8 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)})
7		eleq2 2858	. . . . . . . . . 10 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) ↔ 𝑥 ∈ {(𝐺‘𝑋)}))
8		velsn 4608	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} ↔ 𝑥 = (𝐺‘𝑋))
9		dmressnsn 6023	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋})
10		dffun7 6564	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
11		snidg 4629	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → 𝑋 ∈ {𝑋})
12	11	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ {𝑋})
13		eleq2 2858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({𝑋} = dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
14	13	eqcoms 2777	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
15	14	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
16	12, 15	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))
17		fvex 6895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐺‘𝑋) ∈ V
18	17	isseti 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∃𝑧 𝑧 = (𝐺‘𝑋)
19		eqcom 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝐺‘𝑋) ↔ (𝐺‘𝑋) = 𝑧)
20		fnbrfvb 6932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) = 𝑧 ↔ 𝑋𝐺𝑧))
21	19, 20	bitrid 286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) ↔ 𝑋𝐺𝑧))
22	21	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) → 𝑋𝐺𝑧))
23		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘𝑋) = 𝑧 → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
24	23	eqcoms 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝐺‘𝑋) → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
25	24	biimpcd 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑋)𝐹𝑦 → (𝑧 = (𝐺‘𝑋) → 𝑧𝐹𝑦))
26	22, 25	anim12ii 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑧 = (𝐺‘𝑋) → (𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
27	26	eximdv 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺‘𝑋) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
28	18, 27	mpi 21	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))
29		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
30		vex 3465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑦 ∈ V
31		brcog 5853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
32	29, 30, 31	sylancl 597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
33	32	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
34	28, 33	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋(𝐹 ∘ 𝐺)𝑦)
35	30	brresi 5988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦))
36		snidg 4629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ {𝑋})
37	36	biantrurd 541	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋 ∈ 𝐴 → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦)))
38	35, 37	bitr4id 293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 ∈ 𝐴 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
39	38	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
40	34, 39	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)
41	40	ex 417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
42	41	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
43		breq1 5114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 = 𝑥 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
44	43	eqcoms 2777	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑋 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
45	44	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
46	42, 45	sylibd 242	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
47	46	moimdv 2580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))
48	47	ex 417	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
49	48	com23 87	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
50	16, 49	rspcimdv 3578	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
51	50	ex 417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
52	51	com13 89	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
53	10, 52	simplbiim 513	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
54	53	com13 89	. . . . . . . . . . . . . . . . 17 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
55	9, 54	mpcom 39	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
56	55	imp31 422	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)
57	17	snid 4631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}
58	57	biantrur 539	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
59	58	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
60	59	mobidv 2583	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦(𝐺‘𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
61	56, 60	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
62	61	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
63		breq1 5114	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐺‘𝑋) → (𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ (𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
64	30	brresi 5988	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
65	63, 64	bitr2di 291	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
66	65	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
67	66	mobidv 2583	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
68	62, 67	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
69	68	ex 417	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
70	8, 69	sylbi 220	. . . . . . . . . 10 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
71	7, 70	biimtrdi 256	. . . . . . . . 9 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
72	71	com23 87	. . . . . . . 8 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
73	6, 72	syl 18	. . . . . . 7 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
74	5, 73	syl6com 38	. . . . . 6 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))))
75	74	a1d 26	. . . . 5 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))))
76	75	imp31 422	. . . 4 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
77	76	pm2.43i 53	. . 3 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
78	77	ralrimiv 3162	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
79		dffun7 6564	. 2 ⊢ (Fun (𝐹 ↾ {(𝐺‘𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺‘𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
80	2, 78, 79	sylanbrc 594	1 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∃*wmo 2571  ∀wral 3085  Vcvv 3461  {csn 4592   class class class wbr 5111  dom cdm 5662   ↾ cres 5664   ∘ ccom 5666  Rel wrel 5667  Fun wfun 6531   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741  ax-sep 5259  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-res 5674  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  afvco2  47837