fndmin

Description: Two ways to express the locus of equality between two functions. (Contributed by Stefan O'Rear, 17-Jan-2015)

		Ref	Expression
	Assertion	fndmin	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) = \{x \in A \| F (x) = G (x)\}$

Proof

Step	Hyp	Ref	Expression
1		dffn5	$⊢ F Fn A \leftrightarrow F = (x \in A ⟼ F (x))$
2	1	biimpi	$⊢ F Fn A \to F = (x \in A ⟼ F (x))$
3		df-mpt	$⊢ (x \in A ⟼ F (x)) = \{⟨x, y⟩ \| (x \in A \land y = F (x))\}$
4	2 3	syl6eq	$⊢ F Fn A \to F = \{⟨x, y⟩ \| (x \in A \land y = F (x))\}$
5		dffn5	$⊢ G Fn A \leftrightarrow G = (x \in A ⟼ G (x))$
6	5	biimpi	$⊢ G Fn A \to G = (x \in A ⟼ G (x))$
7		df-mpt	$⊢ (x \in A ⟼ G (x)) = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
8	6 7	syl6eq	$⊢ G Fn A \to G = \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
9	4 8	ineqan12d	$⊢ (F Fn A \land G Fn A) \to F \cap G = \{⟨x, y⟩ \| (x \in A \land y = F (x))\} \cap \{⟨x, y⟩ \| (x \in A \land y = G (x))\}$
10		inopab	$⊢ \{⟨x, y⟩ \| (x \in A \land y = F (x))\} \cap \{⟨x, y⟩ \| (x \in A \land y = G (x))\} = \{⟨x, y⟩ \| ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\}$
11	9 10	syl6eq	$⊢ (F Fn A \land G Fn A) \to F \cap G = \{⟨x, y⟩ \| ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\}$
12	11	dmeqd	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) = dom \{⟨x, y⟩ \| ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\}$
13		19.42v	$⊢ \exists y (x \in A \land (y = F (x) \land y = G (x))) \leftrightarrow (x \in A \land \exists y (y = F (x) \land y = G (x)))$
14		anandi	$⊢ (x \in A \land (y = F (x) \land y = G (x))) \leftrightarrow ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))$
15	14	exbii	$⊢ \exists y (x \in A \land (y = F (x) \land y = G (x))) \leftrightarrow \exists y ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))$
16		fvex	$⊢ F (x) \in V$
17		eqeq1	$⊢ y = F (x) \to (y = G (x) \leftrightarrow F (x) = G (x))$
18	16 17	ceqsexv	$⊢ \exists y (y = F (x) \land y = G (x)) \leftrightarrow F (x) = G (x)$
19	18	anbi2i	$⊢ (x \in A \land \exists y (y = F (x) \land y = G (x))) \leftrightarrow (x \in A \land F (x) = G (x))$
20	13 15 19	3bitr3i	$⊢ \exists y ((x \in A \land y = F (x)) \land (x \in A \land y = G (x))) \leftrightarrow (x \in A \land F (x) = G (x))$
21	20	abbii	$⊢ \{x \| \exists y ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\} = \{x \| (x \in A \land F (x) = G (x))\}$
22		dmopab	$⊢ dom \{⟨x, y⟩ \| ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\} = \{x \| \exists y ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\}$
23		df-rab	$⊢ \{x \in A \| F (x) = G (x)\} = \{x \| (x \in A \land F (x) = G (x))\}$
24	21 22 23	3eqtr4i	$⊢ dom \{⟨x, y⟩ \| ((x \in A \land y = F (x)) \land (x \in A \land y = G (x)))\} = \{x \in A \| F (x) = G (x)\}$
25	12 24	syl6eq	$⊢ (F Fn A \land G Fn A) \to dom (F \cap G) = \{x \in A \| F (x) = G (x)\}$

Metamath Proof Explorer

Theorem fndmin

Proof