dfatco

Description: The predicate "defined at" for a function composition. (Contributed by AV, 8-Sep-2022)

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

Step	Hyp	Ref	Expression
1		dfatcolem	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists! y X (F \circ G) y$
2		euex	$⊢ \exists! y X (F \circ G) y \to \exists y X (F \circ G) y$
3	1 2	syl	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists y X (F \circ G) y$
4		df-dm	$⊢ dom (F \circ G) = \{x \| \exists y x (F \circ G) y\}$
5	4	eleq2i	$⊢ X \in dom (F \circ G) \leftrightarrow X \in \{x \| \exists y x (F \circ G) y\}$
6		df-dfat	$⊢ G defAt X \leftrightarrow (X \in dom G \land Fun ({G ↾}_{\{X\}}))$
7	6	simplbi	$⊢ G defAt X \to X \in dom G$
8	7	adantr	$⊢ (G defAt X \land F defAt (G'''' X)) \to X \in dom G$
9		breq1	$⊢ x = X \to (x (F \circ G) y \leftrightarrow X (F \circ G) y)$
10	9	exbidv	$⊢ x = X \to (\exists y x (F \circ G) y \leftrightarrow \exists y X (F \circ G) y)$
11	10	elabg	$⊢ X \in dom G \to (X \in \{x \| \exists y x (F \circ G) y\} \leftrightarrow \exists y X (F \circ G) y)$
12	8 11	syl	$⊢ (G defAt X \land F defAt (G'''' X)) \to (X \in \{x \| \exists y x (F \circ G) y\} \leftrightarrow \exists y X (F \circ G) y)$
13	5 12	bitrid	$⊢ (G defAt X \land F defAt (G'''' X)) \to (X \in dom (F \circ G) \leftrightarrow \exists y X (F \circ G) y)$
14	3 13	mpbird	$⊢ (G defAt X \land F defAt (G'''' X)) \to X \in dom (F \circ G)$
15		dfdfat2	$⊢ (F \circ G) defAt X \leftrightarrow (X \in dom (F \circ G) \land \exists! y X (F \circ G) y)$
16	14 1 15	sylanbrc	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F \circ G) defAt X$

Metamath Proof Explorer