funressnfv - Mathbox for Alexander van der Vekens

	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 39857

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.)

**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 5346	. . 3 ⊢ Rel (𝐹 ↾ {(𝐺‘𝑋)})
2	1	a1i 11	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Rel (𝐹 ↾ {(𝐺‘𝑋)}))
3		dmfco 6182	. . . . . . . . 9 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹))
4	3	biimpd 218	. . . . . . . 8 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
5	4	funfni 5905	. . . . . . 7 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (𝐺‘𝑋) ∈ dom 𝐹))
6		dmressnsn 5358	. . . . . . . 8 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)})
7		eleq2 2677	. . . . . . . . . 10 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) ↔ 𝑥 ∈ {(𝐺‘𝑋)}))
8		velsn 4141	. . . . . . . . . . 11 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} ↔ 𝑥 = (𝐺‘𝑋))
9		dmressnsn 5358	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋})
10		dffun7 5830	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) ↔ (Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃*𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
11		snidg 4153	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → 𝑋 ∈ {𝑋})
12	11	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ {𝑋})
13		eleq2 2677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ({𝑋} = dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
14	13	eqcoms 2618	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
15	14	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (𝑋 ∈ {𝑋} ↔ 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})))
16	12, 15	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋}))
17		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝐺‘𝑋) ∈ V
18	17	isseti 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ∃𝑧 𝑧 = (𝐺‘𝑋)
19		eqcom 2617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑧 = (𝐺‘𝑋) ↔ (𝐺‘𝑋) = 𝑧)
20		fnbrfvb 6146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) = 𝑧 ↔ 𝑋𝐺𝑧))
21	19, 20	syl5bb 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) ↔ 𝑋𝐺𝑧))
22	21	biimpd 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 = (𝐺‘𝑋) → 𝑋𝐺𝑧))
23		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝐺‘𝑋) = 𝑧 → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
24	23	eqcoms 2618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑧 = (𝐺‘𝑋) → ((𝐺‘𝑋)𝐹𝑦 ↔ 𝑧𝐹𝑦))
25	24	biimpcd 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝐺‘𝑋)𝐹𝑦 → (𝑧 = (𝐺‘𝑋) → 𝑧𝐹𝑦))
26	22, 25	anim12ii 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑧 = (𝐺‘𝑋) → (𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
27	26	eximdv 1833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (∃𝑧 𝑧 = (𝐺‘𝑋) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
28	18, 27	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦))
29		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
30		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑦 ∈ V
31		brcog 5210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ V) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
32	29, 30, 31	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
33	32	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ ∃𝑧(𝑋𝐺𝑧 ∧ 𝑧𝐹𝑦)))
34	28, 33	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋(𝐹 ∘ 𝐺)𝑦)
35		snidg 4153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑋 ∈ 𝐴 → 𝑋 ∈ {𝑋})
36	35	biantrud 527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑋 ∈ 𝐴 → (𝑋(𝐹 ∘ 𝐺)𝑦 ↔ (𝑋(𝐹 ∘ 𝐺)𝑦 ∧ 𝑋 ∈ {𝑋})))
37	30	brres 5323	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ (𝑋(𝐹 ∘ 𝐺)𝑦 ∧ 𝑋 ∈ {𝑋}))
38	36, 37	syl6rbbr 278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑋 ∈ 𝐴 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
39	38	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑋(𝐹 ∘ 𝐺)𝑦))
40	34, 39	mpbird 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ (𝐺‘𝑋)𝐹𝑦) → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦)
41	40	ex 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
42	41	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
43		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑋 = 𝑥 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
44	43	eqcoms 2618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑥 = 𝑋 → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
45	44	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 ↔ 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
46	42, 45	sylibd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
47	46	alrimiv 1842	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑦((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦))
48		moim 2507	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (∀𝑦((𝐺‘𝑋)𝐹𝑦 → 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦) → (∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃𝑦(𝐺‘𝑋)𝐹𝑦))
49	47, 48	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃𝑦(𝐺‘𝑋)𝐹𝑦))
50	49	ex 449	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ∃𝑦(𝐺‘𝑋)𝐹𝑦)))
51	50	com23 84	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) ∧ 𝑥 = 𝑋) → (∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑦(𝐺‘𝑋)𝐹𝑦)))
52	16, 51	rspcimdv 3283	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} ∧ 𝑋 ∈ dom (𝐹 ∘ 𝐺)) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑦(𝐺‘𝑋)𝐹𝑦)))
53	52	ex 449	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑦(𝐺‘𝑋)𝐹𝑦))))
54	53	com13 86	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦 → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑦(𝐺‘𝑋)𝐹𝑦))))
55	54	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Rel ((𝐹 ∘ 𝐺) ↾ {𝑋}) ∧ ∀𝑥 ∈ dom ((𝐹 ∘ 𝐺) ↾ {𝑋})∃𝑦 𝑥((𝐹 ∘ 𝐺) ↾ {𝑋})𝑦) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃𝑦(𝐺‘𝑋)𝐹𝑦))))
56	10, 55	sylbi 206	. . . . . . . . . . . . . . . . . 18 ⊢ (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
57	56	com13 86	. . . . . . . . . . . . . . . . 17 ⊢ (dom ((𝐹 ∘ 𝐺) ↾ {𝑋}) = {𝑋} → (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦))))
58	9, 57	mpcom 37	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)))
59	58	imp31 447	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦(𝐺‘𝑋)𝐹𝑦)
60	17	snid 4155	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}
61	60	biantru 525	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}))
62	61	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐺‘𝑋)𝐹𝑦 ↔ ((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)})))
63	62	mobidv 2479	. . . . . . . . . . . . . . 15 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (∃𝑦(𝐺‘𝑋)𝐹𝑦 ↔ ∃𝑦((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)})))
64	59, 63	mpbid 221	. . . . . . . . . . . . . 14 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}))
65	64	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}))
66		breq1 4586	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (𝐺‘𝑋) → (𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ (𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
67	30	brres 5323	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝑋)(𝐹 ↾ {(𝐺‘𝑋)})𝑦 ↔ ((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}))
68	66, 67	syl6rbb 276	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
69	68	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}) ↔ 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
70	69	mobidv 2479	. . . . . . . . . . . . 13 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → (∃𝑦((𝐺‘𝑋)𝐹𝑦 ∧ (𝐺‘𝑋) ∈ {(𝐺‘𝑋)}) ↔ ∃𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
71	65, 70	mpbid 221	. . . . . . . . . . . 12 ⊢ ((𝑥 = (𝐺‘𝑋) ∧ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴))) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
72	71	ex 449	. . . . . . . . . . 11 ⊢ (𝑥 = (𝐺‘𝑋) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
73	8, 72	sylbi 206	. . . . . . . . . 10 ⊢ (𝑥 ∈ {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
74	7, 73	syl6bi 242	. . . . . . . . 9 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
75	74	com23 84	. . . . . . . 8 ⊢ (dom (𝐹 ↾ {(𝐺‘𝑋)}) = {(𝐺‘𝑋)} → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
76	6, 75	syl 17	. . . . . . 7 ⊢ ((𝐺‘𝑋) ∈ dom 𝐹 → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
77	5, 76	syl6com 36	. . . . . 6 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))))
78	77	a1d 25	. . . . 5 ⊢ (𝑋 ∈ dom (𝐹 ∘ 𝐺) → (Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))))
79	78	imp31 447	. . . 4 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)))
80	79	pm2.43i 50	. . 3 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)}) → ∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
81	80	ralrimiv 2948	. 2 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦)
82		dffun7 5830	. 2 ⊢ (Fun (𝐹 ↾ {(𝐺‘𝑋)}) ↔ (Rel (𝐹 ↾ {(𝐺‘𝑋)}) ∧ ∀𝑥 ∈ dom (𝐹 ↾ {(𝐺‘𝑋)})∃*𝑦 𝑥(𝐹 ↾ {(𝐺‘𝑋)})𝑦))
83	2, 81, 82	sylanbrc 695	1 ⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∀wal 1473 = wceq 1475 ∃wex 1695 ∈ wcel 1977 ∃*wmo 2459 ∀wral 2896 Vcvv 3173 {csn 4125 class class class wbr 4583 dom cdm 5038 ↾ cres 5040 ∘ ccom 5042 Rel wrel 5043 Fun wfun 5798 Fn wfn 5799 ‘cfv 5804

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-sbc 3403 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-opab 4644 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-res 5050 df-iota 5768 df-fun 5806 df-fn 5807 df-fv 5812

This theorem is referenced by: afvco2 39905

W3C validator