funcoressn

Description: A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		dmressnsn	$⊢ G (X) \in dom F \to dom ({F ↾}_{\{G (X)\}}) = \{G (X)\}$
2		df-fn	$⊢ ({F ↾}_{\{G (X)\}}) Fn \{G (X)\} \leftrightarrow (Fun ({F ↾}_{\{G (X)\}}) \land dom ({F ↾}_{\{G (X)\}}) = \{G (X)\})$
3	2	simplbi2com	$⊢ dom ({F ↾}_{\{G (X)\}}) = \{G (X)\} \to (Fun ({F ↾}_{\{G (X)\}}) \to ({F ↾}_{\{G (X)\}}) Fn \{G (X)\})$
4	1 3	syl	$⊢ G (X) \in dom F \to (Fun ({F ↾}_{\{G (X)\}}) \to ({F ↾}_{\{G (X)\}}) Fn \{G (X)\})$
5	4	imp	$⊢ (G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \to ({F ↾}_{\{G (X)\}}) Fn \{G (X)\}$
6	5	adantr	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ({F ↾}_{\{G (X)\}}) Fn \{G (X)\}$
7		fnsnfv	$⊢ (G Fn A \land X \in A) \to \{G (X)\} = G [\{X\}]$
8	7	adantl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to \{G (X)\} = G [\{X\}]$
9		df-ima	$⊢ G [\{X\}] = ran ({G ↾}_{\{X\}})$
10	8 9	eqtrdi	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to \{G (X)\} = ran ({G ↾}_{\{X\}})$
11	10	reseq2d	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to {F ↾}_{\{G (X)\}} = {F ↾}_{ran ({G ↾}_{\{X\}})}$
12	11 10	fneq12d	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (({F ↾}_{\{G (X)\}}) Fn \{G (X)\} \leftrightarrow ({F ↾}_{ran ({G ↾}_{\{X\}})}) Fn ran ({G ↾}_{\{X\}}))$
13	6 12	mpbid	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ({F ↾}_{ran ({G ↾}_{\{X\}})}) Fn ran ({G ↾}_{\{X\}})$
14		fnfun	$⊢ G Fn A \to Fun G$
15		funres	$⊢ Fun G \to Fun ({G ↾}_{\{X\}})$
16	15	funfnd	$⊢ Fun G \to ({G ↾}_{\{X\}}) Fn dom ({G ↾}_{\{X\}})$
17	14 16	syl	$⊢ G Fn A \to ({G ↾}_{\{X\}}) Fn dom ({G ↾}_{\{X\}})$
18	17	adantr	$⊢ (G Fn A \land X \in A) \to ({G ↾}_{\{X\}}) Fn dom ({G ↾}_{\{X\}})$
19	18	adantl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to ({G ↾}_{\{X\}}) Fn dom ({G ↾}_{\{X\}})$
20		fnresfnco	$⊢ (({F ↾}_{ran ({G ↾}_{\{X\}})}) Fn ran ({G ↾}_{\{X\}}) \land ({G ↾}_{\{X\}}) Fn dom ({G ↾}_{\{X\}})) \to (F \circ ({G ↾}_{\{X\}})) Fn dom ({G ↾}_{\{X\}})$
21	13 19 20	syl2anc	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to (F \circ ({G ↾}_{\{X\}})) Fn dom ({G ↾}_{\{X\}})$
22		fnfun	$⊢ (F \circ ({G ↾}_{\{X\}})) Fn dom ({G ↾}_{\{X\}}) \to Fun (F \circ ({G ↾}_{\{X\}}))$
23	21 22	syl	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to Fun (F \circ ({G ↾}_{\{X\}}))$
24		resco	$⊢ {(F \circ G) ↾}_{\{X\}} = F \circ ({G ↾}_{\{X\}})$
25	24	funeqi	$⊢ Fun ({(F \circ G) ↾}_{\{X\}}) \leftrightarrow Fun (F \circ ({G ↾}_{\{X\}}))$
26	23 25	sylibr	$⊢ ((G (X) \in dom F \land Fun ({F ↾}_{\{G (X)\}})) \land (G Fn A \land X \in A)) \to Fun ({(F \circ G) ↾}_{\{X\}})$

Metamath Proof Explorer

Theorem funcoressn

Proof