dfatdmfcoafv2

Description: Domain of a function composition, analogous to dmfco . (Contributed by AV, 7-Sep-2022)

		Ref	Expression
	Assertion	dfatdmfcoafv2	$⊢ G defAt A \to (A \in dom (F \circ G) \leftrightarrow (G'''' A) \in dom F)$

Proof

Step	Hyp	Ref	Expression
1		dfatafv2ex	$⊢ G defAt A \to (G'''' A) \in V$
2		opeq1	$⊢ x = (G'''' A) \to ⟨x, y⟩ = ⟨(G'''' A), y⟩$
3	2	eleq1d	$⊢ x = (G'''' A) \to (⟨x, y⟩ \in F \leftrightarrow ⟨(G'''' A), y⟩ \in F)$
4	3	ceqsexgv	$⊢ (G'''' A) \in V \to (\exists x (x = (G'''' A) \land ⟨x, y⟩ \in F) \leftrightarrow ⟨(G'''' A), y⟩ \in F)$
5	4	bicomd	$⊢ (G'''' A) \in V \to (⟨(G'''' A), y⟩ \in F \leftrightarrow \exists x (x = (G'''' A) \land ⟨x, y⟩ \in F))$
6	1 5	syl	$⊢ G defAt A \to (⟨(G'''' A), y⟩ \in F \leftrightarrow \exists x (x = (G'''' A) \land ⟨x, y⟩ \in F))$
7		eqcom	$⊢ x = (G'''' A) \leftrightarrow (G'''' A) = x$
8		dfatopafv2b	$⊢ (G defAt A \land x \in V) \to ((G'''' A) = x \leftrightarrow ⟨A, x⟩ \in G)$
9	8	elvd	$⊢ G defAt A \to ((G'''' A) = x \leftrightarrow ⟨A, x⟩ \in G)$
10	7 9	bitrid	$⊢ G defAt A \to (x = (G'''' A) \leftrightarrow ⟨A, x⟩ \in G)$
11	10	anbi1d	$⊢ G defAt A \to ((x = (G'''' A) \land ⟨x, y⟩ \in F) \leftrightarrow (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
12	11	exbidv	$⊢ G defAt A \to (\exists x (x = (G'''' A) \land ⟨x, y⟩ \in F) \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
13	6 12	bitrd	$⊢ G defAt A \to (⟨(G'''' A), y⟩ \in F \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
14	13	exbidv	$⊢ G defAt A \to (\exists y ⟨(G'''' A), y⟩ \in F \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
15		eldm2g	$⊢ (G'''' A) \in V \to ((G'''' A) \in dom F \leftrightarrow \exists y ⟨(G'''' A), y⟩ \in F)$
16	1 15	syl	$⊢ G defAt A \to ((G'''' A) \in dom F \leftrightarrow \exists y ⟨(G'''' A), y⟩ \in F)$
17		df-dfat	$⊢ G defAt A \leftrightarrow (A \in dom G \land Fun ({G ↾}_{\{A\}}))$
18		eldm2g	$⊢ A \in dom G \to (A \in dom (F \circ G) \leftrightarrow \exists y ⟨A, y⟩ \in (F \circ G))$
19		opelco2g	$⊢ (A \in dom G \land y \in V) \to (⟨A, y⟩ \in (F \circ G) \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
20	19	elvd	$⊢ A \in dom G \to (⟨A, y⟩ \in (F \circ G) \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
21	20	exbidv	$⊢ A \in dom G \to (\exists y ⟨A, y⟩ \in (F \circ G) \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
22	18 21	bitrd	$⊢ A \in dom G \to (A \in dom (F \circ G) \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
23	22	adantr	$⊢ (A \in dom G \land Fun ({G ↾}_{\{A\}})) \to (A \in dom (F \circ G) \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
24	17 23	sylbi	$⊢ G defAt A \to (A \in dom (F \circ G) \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
25	14 16 24	3bitr4rd	$⊢ G defAt A \to (A \in dom (F \circ G) \leftrightarrow (G'''' A) \in dom F)$

Metamath Proof Explorer

Theorem dfatdmfcoafv2

Proof