imadif

Description: The image of a difference is the difference of images. (Contributed by NM, 24-May-1998)

		Ref	Expression
	Assertion	imadif	$⊢ Fun F^{-1} \to F [A ∖ B] = F [A] ∖ F [B]$

Proof

Step	Hyp	Ref	Expression
1		anandir	$⊢ ((x \in A \land \neg x \in B) \land x F y) \leftrightarrow ((x \in A \land x F y) \land (\neg x \in B \land x F y))$
2	1	exbii	$⊢ \exists x ((x \in A \land \neg x \in B) \land x F y) \leftrightarrow \exists x ((x \in A \land x F y) \land (\neg x \in B \land x F y))$
3		19.40	$⊢ \exists x ((x \in A \land x F y) \land (\neg x \in B \land x F y)) \to (\exists x (x \in A \land x F y) \land \exists x (\neg x \in B \land x F y))$
4	2 3	sylbi	$⊢ \exists x ((x \in A \land \neg x \in B) \land x F y) \to (\exists x (x \in A \land x F y) \land \exists x (\neg x \in B \land x F y))$
5		nfv	$⊢ Ⅎ x Fun F^{-1}$
6		nfe1	$⊢ Ⅎ x \exists x (x F y \land \neg x \in B)$
7	5 6	nfan	$⊢ Ⅎ x (Fun F^{-1} \land \exists x (x F y \land \neg x \in B))$
8		funmo	$⊢ Fun F^{-1} \to \exists^{*} x y F^{-1} x$
9		vex	$⊢ y \in V$
10		vex	$⊢ x \in V$
11	9 10	brcnv	$⊢ y F^{-1} x \leftrightarrow x F y$
12	11	mobii	$⊢ \exists^{} x y F^{-1} x \leftrightarrow \exists^{} x x F y$
13	8 12	sylib	$⊢ Fun F^{-1} \to \exists^{*} x x F y$
14		mopick	$⊢ (\exists^{*} x x F y \land \exists x (x F y \land \neg x \in B)) \to (x F y \to \neg x \in B)$
15	13 14	sylan	$⊢ (Fun F^{-1} \land \exists x (x F y \land \neg x \in B)) \to (x F y \to \neg x \in B)$
16	15	con2d	$⊢ (Fun F^{-1} \land \exists x (x F y \land \neg x \in B)) \to (x \in B \to \neg x F y)$
17		imnan	$⊢ (x \in B \to \neg x F y) \leftrightarrow \neg (x \in B \land x F y)$
18	16 17	sylib	$⊢ (Fun F^{-1} \land \exists x (x F y \land \neg x \in B)) \to \neg (x \in B \land x F y)$
19	7 18	alrimi	$⊢ (Fun F^{-1} \land \exists x (x F y \land \neg x \in B)) \to \forall x \neg (x \in B \land x F y)$
20	19	ex	$⊢ Fun F^{-1} \to (\exists x (x F y \land \neg x \in B) \to \forall x \neg (x \in B \land x F y))$
21		exancom	$⊢ \exists x (x F y \land \neg x \in B) \leftrightarrow \exists x (\neg x \in B \land x F y)$
22		alnex	$⊢ \forall x \neg (x \in B \land x F y) \leftrightarrow \neg \exists x (x \in B \land x F y)$
23	20 21 22	3imtr3g	$⊢ Fun F^{-1} \to (\exists x (\neg x \in B \land x F y) \to \neg \exists x (x \in B \land x F y))$
24	23	anim2d	$⊢ Fun F^{-1} \to ((\exists x (x \in A \land x F y) \land \exists x (\neg x \in B \land x F y)) \to (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y)))$
25	4 24	syl5	$⊢ Fun F^{-1} \to (\exists x ((x \in A \land \neg x \in B) \land x F y) \to (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y)))$
26		19.29r	$⊢ (\exists x (x \in A \land x F y) \land \forall x \neg (x \in B \land x F y)) \to \exists x ((x \in A \land x F y) \land \neg (x \in B \land x F y))$
27	22 26	sylan2br	$⊢ (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y)) \to \exists x ((x \in A \land x F y) \land \neg (x \in B \land x F y))$
28		andi	$⊢ ((x \in A \land x F y) \land (\neg x \in B \lor \neg x F y)) \leftrightarrow (((x \in A \land x F y) \land \neg x \in B) \lor ((x \in A \land x F y) \land \neg x F y))$
29		ianor	$⊢ \neg (x \in B \land x F y) \leftrightarrow (\neg x \in B \lor \neg x F y)$
30	29	anbi2i	$⊢ ((x \in A \land x F y) \land \neg (x \in B \land x F y)) \leftrightarrow ((x \in A \land x F y) \land (\neg x \in B \lor \neg x F y))$
31		an32	$⊢ ((x \in A \land \neg x \in B) \land x F y) \leftrightarrow ((x \in A \land x F y) \land \neg x \in B)$
32		pm3.24	$⊢ \neg (x F y \land \neg x F y)$
33	32	intnan	$⊢ \neg (x \in A \land (x F y \land \neg x F y))$
34		anass	$⊢ ((x \in A \land x F y) \land \neg x F y) \leftrightarrow (x \in A \land (x F y \land \neg x F y))$
35	33 34	mtbir	$⊢ \neg ((x \in A \land x F y) \land \neg x F y)$
36	35	biorfi	$⊢ ((x \in A \land x F y) \land \neg x \in B) \leftrightarrow (((x \in A \land x F y) \land \neg x \in B) \lor ((x \in A \land x F y) \land \neg x F y))$
37	31 36	bitri	$⊢ ((x \in A \land \neg x \in B) \land x F y) \leftrightarrow (((x \in A \land x F y) \land \neg x \in B) \lor ((x \in A \land x F y) \land \neg x F y))$
38	28 30 37	3bitr4i	$⊢ ((x \in A \land x F y) \land \neg (x \in B \land x F y)) \leftrightarrow ((x \in A \land \neg x \in B) \land x F y)$
39	38	exbii	$⊢ \exists x ((x \in A \land x F y) \land \neg (x \in B \land x F y)) \leftrightarrow \exists x ((x \in A \land \neg x \in B) \land x F y)$
40	27 39	sylib	$⊢ (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y)) \to \exists x ((x \in A \land \neg x \in B) \land x F y)$
41	25 40	impbid1	$⊢ Fun F^{-1} \to (\exists x ((x \in A \land \neg x \in B) \land x F y) \leftrightarrow (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y)))$
42		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
43	42	anbi1i	$⊢ (x \in (A ∖ B) \land x F y) \leftrightarrow ((x \in A \land \neg x \in B) \land x F y)$
44	43	exbii	$⊢ \exists x (x \in (A ∖ B) \land x F y) \leftrightarrow \exists x ((x \in A \land \neg x \in B) \land x F y)$
45	9	elima2	$⊢ y \in F [A] \leftrightarrow \exists x (x \in A \land x F y)$
46	9	elima2	$⊢ y \in F [B] \leftrightarrow \exists x (x \in B \land x F y)$
47	46	notbii	$⊢ \neg y \in F [B] \leftrightarrow \neg \exists x (x \in B \land x F y)$
48	45 47	anbi12i	$⊢ (y \in F [A] \land \neg y \in F [B]) \leftrightarrow (\exists x (x \in A \land x F y) \land \neg \exists x (x \in B \land x F y))$
49	41 44 48	3bitr4g	$⊢ Fun F^{-1} \to (\exists x (x \in (A ∖ B) \land x F y) \leftrightarrow (y \in F [A] \land \neg y \in F [B]))$
50	9	elima2	$⊢ y \in F [A ∖ B] \leftrightarrow \exists x (x \in (A ∖ B) \land x F y)$
51		eldif	$⊢ y \in (F [A] ∖ F [B]) \leftrightarrow (y \in F [A] \land \neg y \in F [B])$
52	49 50 51	3bitr4g	$⊢ Fun F^{-1} \to (y \in F [A ∖ B] \leftrightarrow y \in (F [A] ∖ F [B]))$
53	52	eqrdv	$⊢ Fun F^{-1} \to F [A ∖ B] = F [A] ∖ F [B]$

Metamath Proof Explorer

Theorem imadif

Proof