Theorem funressnfv 46993

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 6026	. . 3 ⊢ Rel (𝐹 ↾ {(𝐺‘𝑋)})
2	1	a1i 11	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Rel (𝐹 ↾ {(𝐺‘𝑋)}))
3		dmfco 7005	. . . . . . . . 9 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹))
4	3	biimpd 229	. . . . . . . 8 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
5	4	funfni 6675	. . . . . . 7 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
6		dmressnsn 6043	. . . . . . . 8 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)})
7		eleq2 2828	. . . . . . . . . 10 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) ↔ 𝑥 ∈ {(𝐺‘𝑋)}))
8		velsn 4647	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} ↔ 𝑥 = (𝐺‘𝑋))
9		dmressnsn 6043	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋})
10		dffun7 6595	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
11		snidg 4665	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → 𝑋 ∈ {𝑋})
12	11	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ {𝑋})
13		eleq2 2828	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ({𝑋} = dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
14	13	eqcoms 2743	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
15	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
16	12, 15	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))
17		fvex 6920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝐺‘𝑋) ∈ V
18	17	isseti 3496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ∃𝑧 𝑧 = (𝐺‘𝑋)
19		eqcom 2742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑧 = (𝐺‘𝑋) ↔ (𝐺‘𝑋) = 𝑧)
20		fnbrfvb 6960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) = 𝑧 ↔ 𝑋𝐺𝑧))
21	19, 20	bitrid 283	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) ↔ 𝑋𝐺𝑧))
22	21	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) → 𝑋𝐺𝑧))
23		breq1 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘𝑋) = 𝑧 → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
24	23	eqcoms 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑧 = (𝐺‘𝑋) → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
25	24	biimpcd 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺‘𝑋)𝐹𝑦 → (𝑧 = (𝐺‘𝑋) → 𝑧𝐹𝑦))
26	22, 25	anim12ii 618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑧 = (𝐺‘𝑋) → (𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
27	26	eximdv 1915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺‘𝑋) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
28	18, 27	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))
29		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
30		vex 3482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ 𝑦 ∈ V
31		brcog 5880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ (𝑋 ∈ {𝑋} ∧ 𝑋(𝐹 ∘ 𝐺)𝑦))
36		snidg 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5151	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑋 = 𝑥 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
44	43	eqcoms 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = 𝑋 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
45	44	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
46	42, 45	sylibd 239	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
47	46	moimdv 2544	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))
48	47	ex 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
49	48	com23 86	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → (∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
50	16, 49	rspcimdv 3612	. . . . . . . . . . . . . . . . . . . . 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 4667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}
58	57	biantrur 530	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
59	58	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
60	59	mobidv 2547	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃*𝑦(𝐺‘𝑋)𝐹𝑦 ↔ ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦)))
61	56, 60	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
62	61	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
63		breq1 5151	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐺‘𝑋) → (𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ (𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
64	30	brresi 6009	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ ((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦))
65	63, 64	bitr2di 288	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
66	65	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (((𝐺‘𝑋) ∈ {(𝐺‘𝑋)} ∧ (𝐺‘𝑋)𝐹𝑦) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
67	66	mobidv 2547	. . . . . . . . . . . . 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 3143	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
79		dffun7 6595	. 2 ⊢ (Fun (𝐹 ↾ {(𝐺‘𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺‘𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
80	2, 78, 79	sylanbrc 583	1 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ∃*wmo 2536  ∀wral 3059  Vcvv 3478  {csn 4631   class class class wbr 5148  dom cdm 5689   ↾ cres 5691   ∘ ccom 5693  Rel wrel 5694  Fun wfun 6557   Fn wfn 6558  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-res 5701  df-iota 6516  df-fun 6565  df-fn 6566  df-fv 6571

This theorem is referenced by:  afvco2  47126