funressnfv

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)

		Ref	Expression
	Assertion	funressnfv	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to Fun ({F ↾}_{\{G (X)\}})$

Proof

Step	Hyp	Ref	Expression
1		relres	$⊢ Rel ({F ↾}_{\{G (X)\}})$
2	1	a1i	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to Rel ({F ↾}_{\{G (X)\}})$
3		dmfco	$⊢ (Fun G \land X \in dom G) \to (X \in dom (F \circ G) \leftrightarrow G (X) \in dom F)$
4	3	biimpd	$⊢ (Fun G \land X \in dom G) \to (X \in dom (F \circ G) \to G (X) \in dom F)$
5	4	funfni	$⊢ (G Fn A \land X \in A) \to (X \in dom (F \circ G) \to G (X) \in dom F)$
6		dmressnsn	$⊢ G (X) \in dom F \to dom ({F ↾}_{\{G (X)\}}) = \{G (X)\}$
7		eleq2	$⊢ dom ({F ↾}_{\{G (X)\}}) = \{G (X)\} \to (x \in dom ({F ↾}_{\{G (X)\}}) \leftrightarrow x \in \{G (X)\})$
8		velsn	$⊢ x \in \{G (X)\} \leftrightarrow x = G (X)$
9		dmressnsn	$⊢ X \in dom (F \circ G) \to dom ({(F \circ G) ↾}_{\{X\}}) = \{X\}$
10		dffun7	$⊢ Fun ({(F \circ G) ↾}_{\{X\}}) \leftrightarrow (Rel ({(F \circ G) ↾}_{\{X\}}) \land \forall x \in dom ({(F \circ G) ↾}_{\{X\}}) \exists^{*} y x ({(F \circ G) ↾}_{\{X\}}) y)$
11		snidg	$⊢ X \in dom (F \circ G) \to X \in \{X\}$
12	11	adantl	$⊢ (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \to X \in \{X\}$
13		eleq2	$⊢ \{X\} = dom ({(F \circ G) ↾}_{\{X\}}) \to (X \in \{X\} \leftrightarrow X \in dom ({(F \circ G) ↾}_{\{X\}}))$
14	13	eqcoms	$⊢ dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \to (X \in \{X\} \leftrightarrow X \in dom ({(F \circ G) ↾}_{\{X\}}))$
15	14	adantr	$⊢ (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \to (X \in \{X\} \leftrightarrow X \in dom ({(F \circ G) ↾}_{\{X\}}))$
16	12 15	mpbid	$⊢ (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \to X \in dom ({(F \circ G) ↾}_{\{X\}})$
17		fvex	$⊢ G (X) \in V$
18	17	isseti	$⊢ \exists z z = G (X)$
19		eqcom	$⊢ z = G (X) \leftrightarrow G (X) = z$
20		fnbrfvb	$⊢ (G Fn A \land X \in A) \to (G (X) = z \leftrightarrow X G z)$
21	19 20	bitrid	$⊢ (G Fn A \land X \in A) \to (z = G (X) \leftrightarrow X G z)$
22	21	biimpd	$⊢ (G Fn A \land X \in A) \to (z = G (X) \to X G z)$
23		breq1	$⊢ G (X) = z \to (G (X) F y \leftrightarrow z F y)$
24	23	eqcoms	$⊢ z = G (X) \to (G (X) F y \leftrightarrow z F y)$
25	24	biimpcd	$⊢ G (X) F y \to (z = G (X) \to z F y)$
26	22 25	anim12ii	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to (z = G (X) \to (X G z \land z F y))$
27	26	eximdv	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to (\exists z z = G (X) \to \exists z (X G z \land z F y))$
28	18 27	mpi	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to \exists z (X G z \land z F y)$
29		simpr	$⊢ (G Fn A \land X \in A) \to X \in A$
30		vex	$⊢ y \in V$
31		brcog	$⊢ (X \in A \land y \in V) \to (X (F \circ G) y \leftrightarrow \exists z (X G z \land z F y))$
32	29 30 31	sylancl	$⊢ (G Fn A \land X \in A) \to (X (F \circ G) y \leftrightarrow \exists z (X G z \land z F y))$
33	32	adantr	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to (X (F \circ G) y \leftrightarrow \exists z (X G z \land z F y))$
34	28 33	mpbird	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to X (F \circ G) y$
35	30	brresi	$⊢ X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow (X \in \{X\} \land X (F \circ G) y)$
36		snidg	$⊢ X \in A \to X \in \{X\}$
37	36	biantrurd	$⊢ X \in A \to (X (F \circ G) y \leftrightarrow (X \in \{X\} \land X (F \circ G) y))$
38	35 37	bitr4id	$⊢ X \in A \to (X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow X (F \circ G) y)$
39	38	ad2antlr	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to (X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow X (F \circ G) y)$
40	34 39	mpbird	$⊢ ((G Fn A \land X \in A) \land G (X) F y) \to X ({(F \circ G) ↾}_{\{X\}}) y$
41	40	ex	$⊢ (G Fn A \land X \in A) \to (G (X) F y \to X ({(F \circ G) ↾}_{\{X\}}) y)$
42	41	adantl	$⊢ (((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \land (G Fn A \land X \in A)) \to (G (X) F y \to X ({(F \circ G) ↾}_{\{X\}}) y)$
43		breq1	$⊢ X = x \to (X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow x ({(F \circ G) ↾}_{\{X\}}) y)$
44	43	eqcoms	$⊢ x = X \to (X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow x ({(F \circ G) ↾}_{\{X\}}) y)$
45	44	ad2antlr	$⊢ (((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \land (G Fn A \land X \in A)) \to (X ({(F \circ G) ↾}_{\{X\}}) y \leftrightarrow x ({(F \circ G) ↾}_{\{X\}}) y)$
46	42 45	sylibd	$⊢ (((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \land (G Fn A \land X \in A)) \to (G (X) F y \to x ({(F \circ G) ↾}_{\{X\}}) y)$
47	46	moimdv	$⊢ (((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \land (G Fn A \land X \in A)) \to (\exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to \exists^{} y G (X) F y)$
48	47	ex	$⊢ ((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \to ((G Fn A \land X \in A) \to (\exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to \exists^{} y G (X) F y))$
49	48	com23	$⊢ ((dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \land x = X) \to (\exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to ((G Fn A \land X \in A) \to \exists^{} y G (X) F y))$
50	16 49	rspcimdv	$⊢ (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \land X \in dom (F \circ G)) \to (\forall x \in dom ({(F \circ G) ↾}_{\{X\}}) \exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to ((G Fn A \land X \in A) \to \exists^{} y G (X) F y))$
51	50	ex	$⊢ dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \to (X \in dom (F \circ G) \to (\forall x \in dom ({(F \circ G) ↾}_{\{X\}}) \exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to ((G Fn A \land X \in A) \to \exists^{} y G (X) F y)))$
52	51	com13	$⊢ \forall x \in dom ({(F \circ G) ↾}_{\{X\}}) \exists^{} y x ({(F \circ G) ↾}_{\{X\}}) y \to (X \in dom (F \circ G) \to (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \to ((G Fn A \land X \in A) \to \exists^{} y G (X) F y)))$
53	10 52	simplbiim	$⊢ Fun ({(F \circ G) ↾}_{\{X\}}) \to (X \in dom (F \circ G) \to (dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \to ((G Fn A \land X \in A) \to \exists^{*} y G (X) F y)))$
54	53	com13	$⊢ dom ({(F \circ G) ↾}_{\{X\}}) = \{X\} \to (X \in dom (F \circ G) \to (Fun ({(F \circ G) ↾}_{\{X\}}) \to ((G Fn A \land X \in A) \to \exists^{*} y G (X) F y)))$
55	9 54	mpcom	$⊢ X \in dom (F \circ G) \to (Fun ({(F \circ G) ↾}_{\{X\}}) \to ((G Fn A \land X \in A) \to \exists^{*} y G (X) F y))$
56	55	imp31	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \exists^{*} y G (X) F y$
57	17	snid	$⊢ G (X) \in \{G (X)\}$
58	57	biantrur	$⊢ G (X) F y \leftrightarrow (G (X) \in \{G (X)\} \land G (X) F y)$
59	58	a1i	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (G (X) F y \leftrightarrow (G (X) \in \{G (X)\} \land G (X) F y))$
60	59	mobidv	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (\exists^{} y G (X) F y \leftrightarrow \exists^{} y (G (X) \in \{G (X)\} \land G (X) F y))$
61	56 60	mpbid	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \exists^{*} y (G (X) \in \{G (X)\} \land G (X) F y)$
62	61	adantl	$⊢ (x = G (X) \land ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A))) \to \exists^{*} y (G (X) \in \{G (X)\} \land G (X) F y)$
63		breq1	$⊢ x = G (X) \to (x ({F ↾}_{\{G (X)\}}) y \leftrightarrow G (X) ({F ↾}_{\{G (X)\}}) y)$
64	30	brresi	$⊢ G (X) ({F ↾}_{\{G (X)\}}) y \leftrightarrow (G (X) \in \{G (X)\} \land G (X) F y)$
65	63 64	bitr2di	$⊢ x = G (X) \to ((G (X) \in \{G (X)\} \land G (X) F y) \leftrightarrow x ({F ↾}_{\{G (X)\}}) y)$
66	65	adantr	$⊢ (x = G (X) \land ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A))) \to ((G (X) \in \{G (X)\} \land G (X) F y) \leftrightarrow x ({F ↾}_{\{G (X)\}}) y)$
67	66	mobidv	$⊢ (x = G (X) \land ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A))) \to (\exists^{} y (G (X) \in \{G (X)\} \land G (X) F y) \leftrightarrow \exists^{} y x ({F ↾}_{\{G (X)\}}) y)$
68	62 67	mpbid	$⊢ (x = G (X) \land ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A))) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y$
69	68	ex	$⊢ x = G (X) \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y)$
70	8 69	sylbi	$⊢ x \in \{G (X)\} \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y)$
71	7 70	syl6bi	$⊢ dom ({F ↾}_{\{G (X)\}}) = \{G (X)\} \to (x \in dom ({F ↾}_{\{G (X)\}}) \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y))$
72	71	com23	$⊢ dom ({F ↾}_{\{G (X)\}}) = \{G (X)\} \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y))$
73	6 72	syl	$⊢ G (X) \in dom F \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y))$
74	5 73	syl6com	$⊢ X \in dom (F \circ G) \to ((G Fn A \land X \in A) \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y)))$
75	74	a1d	$⊢ X \in dom (F \circ G) \to (Fun ({(F \circ G) ↾}_{\{X\}}) \to ((G Fn A \land X \in A) \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y))))$
76	75	imp31	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y))$
77	76	pm2.43i	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to (x \in dom ({F ↾}_{\{G (X)\}}) \to \exists^{*} y x ({F ↾}_{\{G (X)\}}) y)$
78	77	ralrimiv	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to \forall x \in dom ({F ↾}_{\{G (X)\}}) \exists^{*} y x ({F ↾}_{\{G (X)\}}) y$
79		dffun7	$⊢ Fun ({F ↾}_{\{G (X)\}}) \leftrightarrow (Rel ({F ↾}_{\{G (X)\}}) \land \forall x \in dom ({F ↾}_{\{G (X)\}}) \exists^{*} y x ({F ↾}_{\{G (X)\}}) y)$
80	2 78 79	sylanbrc	$⊢ ((X \in dom (F \circ G) \land Fun ({(F \circ G) ↾}_{\{X\}})) \land (G Fn A \land X \in A)) \to Fun ({F ↾}_{\{G (X)\}})$

Metamath Proof Explorer

Theorem funressnfv

Proof