afv2co2

Description: Value of a function composition, analogous to fvco2 . (Contributed by AV, 8-Sep-2022)

		Ref	Expression
	Assertion	afv2co2	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((F \circ G)'''' X) = (F'''' (G'''' X))$

Step	Hyp	Ref	Expression
1		imaco	$⊢ (F \circ G) [\{X\}] = F [G [\{X\}]]$
2		dfatsnafv2	$⊢ G defAt X \to \{(G'''' X)\} = G [\{X\}]$
3	2	adantr	$⊢ (G defAt X \land F defAt (G'''' X)) \to \{(G'''' X)\} = G [\{X\}]$
4	3	imaeq2d	$⊢ (G defAt X \land F defAt (G'''' X)) \to F [\{(G'''' X)\}] = F [G [\{X\}]]$
5	1 4	eqtr4id	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F \circ G) [\{X\}] = F [\{(G'''' X)\}]$
6	5	eleq2d	$⊢ (G defAt X \land F defAt (G'''' X)) \to (x \in (F \circ G) [\{X\}] \leftrightarrow x \in F [\{(G'''' X)\}])$
7	6	iotabidv	$⊢ (G defAt X \land F defAt (G'''' X)) \to (ι x \| x \in (F \circ G) [\{X\}]) = (ι x \| x \in F [\{(G'''' X)\}])$
8		dfatco	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F \circ G) defAt X$
9		dfafv23	$⊢ (F \circ G) defAt X \to ((F \circ G)'''' X) = (ι x \| x \in (F \circ G) [\{X\}])$
10	8 9	syl	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((F \circ G)'''' X) = (ι x \| x \in (F \circ G) [\{X\}])$
11		dfafv23	$⊢ F defAt (G'''' X) \to (F'''' (G'''' X)) = (ι x \| x \in F [\{(G'''' X)\}])$
12	11	adantl	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F'''' (G'''' X)) = (ι x \| x \in F [\{(G'''' X)\}])$
13	7 10 12	3eqtr4d	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((F \circ G)'''' X) = (F'''' (G'''' X))$

Metamath Proof Explorer