dmfcoafv

Description: Domains of a function composition, analogous to dmfco . (Contributed by Alexander van der Vekens, 23-Jul-2017)

		Ref	Expression
	Assertion	dmfcoafv	$⊢ (Fun G \land A \in dom G) \to (A \in dom (F \circ G) \leftrightarrow (G''' A) \in dom F)$

Step	Hyp	Ref	Expression
1		dmfco	$⊢ (Fun G \land A \in dom G) \to (A \in dom (F \circ G) \leftrightarrow G (A) \in dom F)$
2		funres	$⊢ Fun G \to Fun ({G ↾}_{\{A\}})$
3	2	anim2i	$⊢ (A \in dom G \land Fun G) \to (A \in dom G \land Fun ({G ↾}_{\{A\}}))$
4	3	ancoms	$⊢ (Fun G \land A \in dom G) \to (A \in dom G \land Fun ({G ↾}_{\{A\}}))$
5		df-dfat	$⊢ G defAt A \leftrightarrow (A \in dom G \land Fun ({G ↾}_{\{A\}}))$
6		afvfundmfveq	$⊢ G defAt A \to (G''' A) = G (A)$
7	5 6	sylbir	$⊢ (A \in dom G \land Fun ({G ↾}_{\{A\}})) \to (G''' A) = G (A)$
8	4 7	syl	$⊢ (Fun G \land A \in dom G) \to (G''' A) = G (A)$
9	8	eqcomd	$⊢ (Fun G \land A \in dom G) \to G (A) = (G''' A)$
10	9	eleq1d	$⊢ (Fun G \land A \in dom G) \to (G (A) \in dom F \leftrightarrow (G''' A) \in dom F)$
11	1 10	bitrd	$⊢ (Fun G \land A \in dom G) \to (A \in dom (F \circ G) \leftrightarrow (G''' A) \in dom F)$

Metamath Proof Explorer