Theorem imadif 2714

Description: The image of a difference is the difference of images.

Assertion

Ref	Expression
imadif	⊢ (Fun ◡F → (F “ (A ∖ B)) = ((F “ A) ∖ (F “ B)))

Proof of Theorem imadif

Step	Hyp	Ref	Expression
1		ax-17 925	. . . . . . . . . . 11 ⊢ (Fun ◡F → ∀xFun ◡F)
2		hbe1 709	. . . . . . . . . . 11 ⊢ (∃x(xFy ∧ ¬ x ∈ B) → ∀x∃x(xFy ∧ ¬ x ∈ B))
3	1, 2	hban 704	. . . . . . . . . 10 ⊢ ((Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)) → ∀x(Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)))
4		mopick 1054	. . . . . . . . . . . . 13 ⊢ ((∃*x xFy ∧ ∃x(xFy ∧ ¬ x ∈ B)) → (xFy → ¬ x ∈ B))
5		funmo 2680	. . . . . . . . . . . . . 14 ⊢ (Fun ◡F → ∃*x y◡Fx)
6		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ y ∈ V
7		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
8	6, 7	brcnv 2519	. . . . . . . . . . . . . . 15 ⊢ (y◡Fx ↔ xFy)
9	8	bimo 1031	. . . . . . . . . . . . . 14 ⊢ (∃*x y◡Fx ↔ ∃*x xFy)
10	5, 9	sylib 173	. . . . . . . . . . . . 13 ⊢ (Fun ◡F → ∃*x xFy)
11	4, 10	sylan 343	. . . . . . . . . . . 12 ⊢ ((Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)) → (xFy → ¬ x ∈ B))
12	11	con2d 83	. . . . . . . . . . 11 ⊢ ((Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)) → (x ∈ B → ¬ xFy))
13		imnan 207	. . . . . . . . . . 11 ⊢ ((x ∈ B → ¬ xFy) ↔ ¬ (x ∈ B ∧ xFy))
14	12, 13	sylib 173	. . . . . . . . . 10 ⊢ ((Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)) → ¬ (x ∈ B ∧ xFy))
15	3, 14	19.21ai 740	. . . . . . . . 9 ⊢ ((Fun ◡F ∧ ∃x(xFy ∧ ¬ x ∈ B)) → ∀x ¬ (x ∈ B ∧ xFy))
16	15	exp 291	. . . . . . . 8 ⊢ (Fun ◡F → (∃x(xFy ∧ ¬ x ∈ B) → ∀x ¬ (x ∈ B ∧ xFy)))
17		exancom 736	. . . . . . . 8 ⊢ (∃x(xFy ∧ ¬ x ∈ B) ↔ ∃x(¬ x ∈ B ∧ xFy))
18		alnex 716	. . . . . . . 8 ⊢ (∀x ¬ (x ∈ B ∧ xFy) ↔ ¬ ∃x(x ∈ B ∧ xFy))
19	16, 17, 18	3imtr3g 425	. . . . . . 7 ⊢ (Fun ◡F → (∃x(¬ x ∈ B ∧ xFy) → ¬ ∃x(x ∈ B ∧ xFy)))
20	19	anim2d 433	. . . . . 6 ⊢ (Fun ◡F → ((∃x(x ∈ A ∧ xFy) ∧ ∃x(¬ x ∈ B ∧ xFy)) → (∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy))))
21		anandir 393	. . . . . . . 8 ⊢ (((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) ↔ ((x ∈ A ∧ xFy) ∧ (¬ x ∈ B ∧ xFy)))
22	21	biex 733	. . . . . . 7 ⊢ (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) ↔ ∃x((x ∈ A ∧ xFy) ∧ (¬ x ∈ B ∧ xFy)))
23		19.40 773	. . . . . . 7 ⊢ (∃x((x ∈ A ∧ xFy) ∧ (¬ x ∈ B ∧ xFy)) → (∃x(x ∈ A ∧ xFy) ∧ ∃x(¬ x ∈ B ∧ xFy)))
24	22, 23	sylbi 174	. . . . . 6 ⊢ (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) → (∃x(x ∈ A ∧ xFy) ∧ ∃x(¬ x ∈ B ∧ xFy)))
25	20, 24	syl5 22	. . . . 5 ⊢ (Fun ◡F → (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) → (∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy))))
26		19.29r 753	. . . . . . . 8 ⊢ ((∃x(x ∈ A ∧ xFy) ∧ ∀x ¬ (x ∈ B ∧ xFy)) → ∃x((x ∈ A ∧ xFy) ∧ ¬ (x ∈ B ∧ xFy)))
27	26, 18	sylan2br 348	. . . . . . 7 ⊢ ((∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy)) → ∃x((x ∈ A ∧ xFy) ∧ ¬ (x ∈ B ∧ xFy)))
28		andi 456	. . . . . . . . 9 ⊢ (((x ∈ A ∧ xFy) ∧ (¬ x ∈ B ∨ ¬ xFy)) ↔ (((x ∈ A ∧ xFy) ∧ ¬ x ∈ B) ∨ ((x ∈ A ∧ xFy) ∧ ¬ xFy)))
29		ianor 253	. . . . . . . . . 10 ⊢ (¬ (x ∈ B ∧ xFy) ↔ (¬ x ∈ B ∨ ¬ xFy))
30	29	anbi2i 367	. . . . . . . . 9 ⊢ (((x ∈ A ∧ xFy) ∧ ¬ (x ∈ B ∧ xFy)) ↔ ((x ∈ A ∧ xFy) ∧ (¬ x ∈ B ∨ ¬ xFy)))
31		an23 371	. . . . . . . . . 10 ⊢ (((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) ↔ ((x ∈ A ∧ xFy) ∧ ¬ x ∈ B))
32		pm3.24 496	. . . . . . . . . . . . 13 ⊢ ¬ (xFy ∧ ¬ xFy)
33	32	intnan 516	. . . . . . . . . . . 12 ⊢ ¬ (x ∈ A ∧ (xFy ∧ ¬ xFy))
34		anass 336	. . . . . . . . . . . 12 ⊢ (((x ∈ A ∧ xFy) ∧ ¬ xFy) ↔ (x ∈ A ∧ (xFy ∧ ¬ xFy)))
35	33, 34	mtbir 167	. . . . . . . . . . 11 ⊢ ¬ ((x ∈ A ∧ xFy) ∧ ¬ xFy)
36	35	biorfi 552	. . . . . . . . . 10 ⊢ (((x ∈ A ∧ xFy) ∧ ¬ x ∈ B) ↔ (((x ∈ A ∧ xFy) ∧ ¬ x ∈ B) ∨ ((x ∈ A ∧ xFy) ∧ ¬ xFy)))
37	31, 36	bitr 151	. . . . . . . . 9 ⊢ (((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) ↔ (((x ∈ A ∧ xFy) ∧ ¬ x ∈ B) ∨ ((x ∈ A ∧ xFy) ∧ ¬ xFy)))
38	28, 30, 37	3bitr4 158	. . . . . . . 8 ⊢ (((x ∈ A ∧ xFy) ∧ ¬ (x ∈ B ∧ xFy)) ↔ ((x ∈ A ∧ ¬ x ∈ B) ∧ xFy))
39	38	biex 733	. . . . . . 7 ⊢ (∃x((x ∈ A ∧ xFy) ∧ ¬ (x ∈ B ∧ xFy)) ↔ ∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy))
40	27, 39	sylib 173	. . . . . 6 ⊢ ((∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy)) → ∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy))
41	40	a1i 7	. . . . 5 ⊢ (Fun ◡F → ((∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy)) → ∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy)))
42	25, 41	impbid 397	. . . 4 ⊢ (Fun ◡F → (∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy) ↔ (∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy))))
43		eldif 1496	. . . . . 6 ⊢ (x ∈ (A ∖ B) ↔ (x ∈ A ∧ ¬ x ∈ B))
44	43	anbi1i 368	. . . . 5 ⊢ ((x ∈ (A ∖ B) ∧ xFy) ↔ ((x ∈ A ∧ ¬ x ∈ B) ∧ xFy))
45	44	biex 733	. . . 4 ⊢ (∃x(x ∈ (A ∖ B) ∧ xFy) ↔ ∃x((x ∈ A ∧ ¬ x ∈ B) ∧ xFy))
46	6	elima2 2607	. . . . 5 ⊢ (y ∈ (F “ A) ↔ ∃x(x ∈ A ∧ xFy))
47	6	elima2 2607	. . . . . 6 ⊢ (y ∈ (F “ B) ↔ ∃x(x ∈ B ∧ xFy))
48	47	negbii 162	. . . . 5 ⊢ (¬ y ∈ (F “ B) ↔ ¬ ∃x(x ∈ B ∧ xFy))
49	46, 48	anbi12i 369	. . . 4 ⊢ ((y ∈ (F “ A) ∧ ¬ y ∈ (F “ B)) ↔ (∃x(x ∈ A ∧ xFy) ∧ ¬ ∃x(x ∈ B ∧ xFy)))
50	42, 45, 49	3bitr4g 428	. . 3 ⊢ (Fun ◡F → (∃x(x ∈ (A ∖ B) ∧ xFy) ↔ (y ∈ (F “ A) ∧ ¬ y ∈ (F “ B))))
51	6	elima2 2607	. . 3 ⊢ (y ∈ (F “ (A ∖ B)) ↔ ∃x(x ∈ (A ∖ B) ∧ xFy))
52		eldif 1496	. . 3 ⊢ (y ∈ ((F “ A) ∖ (F “ B)) ↔ (y ∈ (F “ A) ∧ ¬ y ∈ (F “ B)))
53	50, 51, 52	3bitr4g 428	. 2 ⊢ (Fun ◡F → (y ∈ (F “ (A ∖ B)) ↔ y ∈ ((F “ A) ∖ (F “ B))))
54	53	cleqrd 1100	1 ⊢ (Fun ◡F → (F “ (A ∖ B)) = ((F “ A) ∖ (F “ B)))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃wex 678  ∃*wmo 1008   = wceq 1091   ∈ wcel 1092   ∖ cdif 1484   class class class wbr 2054  ^◡ccnv 2409   “ cima 2413  Fun wfun 2416

This theorem is referenced by:  phplem5 3407  php3 3411

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432

metamath.org