fndmdif

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

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

Proof

Step	Hyp	Ref	Expression
1		difss	$⊢ F ∖ G \subseteq F$
2		dmss	$⊢ F ∖ G \subseteq F \to dom (F ∖ G) \subseteq dom F$
3	1 2	ax-mp	$⊢ dom (F ∖ G) \subseteq dom F$
4		fndm	$⊢ F Fn A \to dom F = A$
5	4	adantr	$⊢ (F Fn A \land G Fn A) \to dom F = A$
6	3 5	sseqtrid	$⊢ (F Fn A \land G Fn A) \to dom (F ∖ G) \subseteq A$
7		sseqin2	$⊢ dom (F ∖ G) \subseteq A \leftrightarrow A \cap dom (F ∖ G) = dom (F ∖ G)$
8	6 7	sylib	$⊢ (F Fn A \land G Fn A) \to A \cap dom (F ∖ G) = dom (F ∖ G)$
9		vex	$⊢ x \in V$
10	9	eldm	$⊢ x \in dom (F ∖ G) \leftrightarrow \exists y x (F ∖ G) y$
11		eqcom	$⊢ F (x) = G (x) \leftrightarrow G (x) = F (x)$
12		fnbrfvb	$⊢ (G Fn A \land x \in A) \to (G (x) = F (x) \leftrightarrow x G F (x))$
13	11 12	bitrid	$⊢ (G Fn A \land x \in A) \to (F (x) = G (x) \leftrightarrow x G F (x))$
14	13	adantll	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (F (x) = G (x) \leftrightarrow x G F (x))$
15	14	necon3abid	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (F (x) \neq G (x) \leftrightarrow \neg x G F (x))$
16		fvex	$⊢ F (x) \in V$
17		breq2	$⊢ y = F (x) \to (x G y \leftrightarrow x G F (x))$
18	17	notbid	$⊢ y = F (x) \to (\neg x G y \leftrightarrow \neg x G F (x))$
19	16 18	ceqsexv	$⊢ \exists y (y = F (x) \land \neg x G y) \leftrightarrow \neg x G F (x)$
20	15 19	bitr4di	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (F (x) \neq G (x) \leftrightarrow \exists y (y = F (x) \land \neg x G y))$
21		eqcom	$⊢ y = F (x) \leftrightarrow F (x) = y$
22		fnbrfvb	$⊢ (F Fn A \land x \in A) \to (F (x) = y \leftrightarrow x F y)$
23	21 22	bitrid	$⊢ (F Fn A \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
24	23	adantlr	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (y = F (x) \leftrightarrow x F y)$
25	24	anbi1d	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to ((y = F (x) \land \neg x G y) \leftrightarrow (x F y \land \neg x G y))$
26		brdif	$⊢ x (F ∖ G) y \leftrightarrow (x F y \land \neg x G y)$
27	25 26	bitr4di	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to ((y = F (x) \land \neg x G y) \leftrightarrow x (F ∖ G) y)$
28	27	exbidv	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (\exists y (y = F (x) \land \neg x G y) \leftrightarrow \exists y x (F ∖ G) y)$
29	20 28	bitr2d	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (\exists y x (F ∖ G) y \leftrightarrow F (x) \neq G (x))$
30	10 29	bitrid	$⊢ ((F Fn A \land G Fn A) \land x \in A) \to (x \in dom (F ∖ G) \leftrightarrow F (x) \neq G (x))$
31	30	rabbi2dva	$⊢ (F Fn A \land G Fn A) \to A \cap dom (F ∖ G) = \{x \in A \| F (x) \neq G (x)\}$
32	8 31	eqtr3d	$⊢ (F Fn A \land G Fn A) \to dom (F ∖ G) = \{x \in A \| F (x) \neq G (x)\}$

Metamath Proof Explorer

Theorem fndmdif

Proof