dmfco

Description: Domains of a function composition. (Contributed by NM, 27-Jan-1997)

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

Proof

Step	Hyp	Ref	Expression
1		eldm2g	$⊢ A \in dom G \to (A \in dom (F \circ G) \leftrightarrow \exists y ⟨A, y⟩ \in (F \circ G))$
2		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))$
3	2	elvd	$⊢ A \in dom G \to (⟨A, y⟩ \in (F \circ G) \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
4	3	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))$
5	1 4	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))$
6	5	adantl	$⊢ (Fun G \land 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))$
7		fvex	$⊢ G (A) \in V$
8	7	eldm2	$⊢ G (A) \in dom F \leftrightarrow \exists y ⟨G (A), y⟩ \in F$
9		opeq1	$⊢ x = G (A) \to ⟨x, y⟩ = ⟨G (A), y⟩$
10	9	eleq1d	$⊢ x = G (A) \to (⟨x, y⟩ \in F \leftrightarrow ⟨G (A), y⟩ \in F)$
11	7 10	ceqsexv	$⊢ \exists x (x = G (A) \land ⟨x, y⟩ \in F) \leftrightarrow ⟨G (A), y⟩ \in F$
12		eqcom	$⊢ x = G (A) \leftrightarrow G (A) = x$
13		funopfvb	$⊢ (Fun G \land A \in dom G) \to (G (A) = x \leftrightarrow ⟨A, x⟩ \in G)$
14	12 13	bitrid	$⊢ (Fun G \land A \in dom G) \to (x = G (A) \leftrightarrow ⟨A, x⟩ \in G)$
15	14	anbi1d	$⊢ (Fun G \land A \in dom G) \to ((x = G (A) \land ⟨x, y⟩ \in F) \leftrightarrow (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
16	15	exbidv	$⊢ (Fun G \land A \in dom G) \to (\exists x (x = G (A) \land ⟨x, y⟩ \in F) \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
17	11 16	bitr3id	$⊢ (Fun G \land A \in dom G) \to (⟨G (A), y⟩ \in F \leftrightarrow \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
18	17	exbidv	$⊢ (Fun G \land A \in dom G) \to (\exists y ⟨G (A), y⟩ \in F \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
19	8 18	bitrid	$⊢ (Fun G \land A \in dom G) \to (G (A) \in dom F \leftrightarrow \exists y \exists x (⟨A, x⟩ \in G \land ⟨x, y⟩ \in F))$
20	6 19	bitr4d	$⊢ (Fun G \land A \in dom G) \to (A \in dom (F \circ G) \leftrightarrow G (A) \in dom F)$

Metamath Proof Explorer

Theorem dmfco

Proof