Theorem f1fv 2916

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of [Monk1] p. 43.

Assertion

Ref	Expression
f1fv	⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))

Distinct variable group(s):   x,y,A   x,B,y   x,F,y

Proof of Theorem f1fv

Step	Hyp	Ref	Expression
1		f11 2780	. 2 ⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀z∃*x xFz))
2		ffn 2752	. . . 4 ⊢ (F:A–→B → F Fn A)
3		fndm 2723	. . . . . . . . . . . . . . . 16 ⊢ (F Fn A → dom F = A)
4	3	eleq2d 1156	. . . . . . . . . . . . . . 15 ⊢ (F Fn A → (x ∈ dom F ↔ x ∈ A))
5		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
6	5	breldm 2535	. . . . . . . . . . . . . . 15 ⊢ (xFz → x ∈ dom F)
7	4, 6	syl5bi 183	. . . . . . . . . . . . . 14 ⊢ (F Fn A → (xFz → x ∈ A))
8	3	eleq2d 1156	. . . . . . . . . . . . . . 15 ⊢ (F Fn A → (y ∈ dom F ↔ y ∈ A))
9		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ y ∈ V
10	9	breldm 2535	. . . . . . . . . . . . . . 15 ⊢ (yFz → y ∈ dom F)
11	8, 10	syl5bi 183	. . . . . . . . . . . . . 14 ⊢ (F Fn A → (yFz → y ∈ A))
12	7, 11	anim12d 431	. . . . . . . . . . . . 13 ⊢ (F Fn A → ((xFz ∧ yFz) → (x ∈ A ∧ y ∈ A)))
13	12	ancrd 247	. . . . . . . . . . . 12 ⊢ (F Fn A → ((xFz ∧ yFz) → ((x ∈ A ∧ y ∈ A) ∧ (xFz ∧ yFz))))
14		pm3.27 260	. . . . . . . . . . . . 13 ⊢ (((x ∈ A ∧ y ∈ A) ∧ (xFz ∧ yFz)) → (xFz ∧ yFz))
15	14	a1i 7	. . . . . . . . . . . 12 ⊢ (F Fn A → (((x ∈ A ∧ y ∈ A) ∧ (xFz ∧ yFz)) → (xFz ∧ yFz)))
16	13, 15	impbid 397	. . . . . . . . . . 11 ⊢ (F Fn A → ((xFz ∧ yFz) ↔ ((x ∈ A ∧ y ∈ A) ∧ (xFz ∧ yFz))))
17		visset 1350	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
18	17	fnfvbr 2855	. . . . . . . . . . . . . . . 16 ⊢ ((F Fn A ∧ x ∈ A) → ((F ‘x) = z ↔ xFz))
19		cleqcom 1103	. . . . . . . . . . . . . . . 16 ⊢ (z = (F ‘x) ↔ (F ‘x) = z)
20	18, 19	syl5bb 410	. . . . . . . . . . . . . . 15 ⊢ ((F Fn A ∧ x ∈ A) → (z = (F ‘x) ↔ xFz))
21	17	fnfvbr 2855	. . . . . . . . . . . . . . . 16 ⊢ ((F Fn A ∧ y ∈ A) → ((F ‘y) = z ↔ yFz))
22		cleqcom 1103	. . . . . . . . . . . . . . . 16 ⊢ (z = (F ‘y) ↔ (F ‘y) = z)
23	21, 22	syl5bb 410	. . . . . . . . . . . . . . 15 ⊢ ((F Fn A ∧ y ∈ A) → (z = (F ‘y) ↔ yFz))
24	20, 23	bi2anan9 478	. . . . . . . . . . . . . 14 ⊢ (((F Fn A ∧ x ∈ A) ∧ (F Fn A ∧ y ∈ A)) → ((z = (F ‘x) ∧ z = (F ‘y)) ↔ (xFz ∧ yFz)))
25	24	anandis 394	. . . . . . . . . . . . 13 ⊢ ((F Fn A ∧ (x ∈ A ∧ y ∈ A)) → ((z = (F ‘x) ∧ z = (F ‘y)) ↔ (xFz ∧ yFz)))
26	25	exp 291	. . . . . . . . . . . 12 ⊢ (F Fn A → ((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) ↔ (xFz ∧ yFz))))
27	26	pm5.32d 491	. . . . . . . . . . 11 ⊢ (F Fn A → (((x ∈ A ∧ y ∈ A) ∧ (z = (F ‘x) ∧ z = (F ‘y))) ↔ ((x ∈ A ∧ y ∈ A) ∧ (xFz ∧ yFz))))
28	16, 27	bitr4d 409	. . . . . . . . . 10 ⊢ (F Fn A → ((xFz ∧ yFz) ↔ ((x ∈ A ∧ y ∈ A) ∧ (z = (F ‘x) ∧ z = (F ‘y)))))
29	28	imbi1d 465	. . . . . . . . 9 ⊢ (F Fn A → (((xFz ∧ yFz) → x = y) ↔ (((x ∈ A ∧ y ∈ A) ∧ (z = (F ‘x) ∧ z = (F ‘y))) → x = y)))
30		impexp 276	. . . . . . . . 9 ⊢ ((((x ∈ A ∧ y ∈ A) ∧ (z = (F ‘x) ∧ z = (F ‘y))) → x = y) ↔ ((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) → x = y)))
31	29, 30	syl6bb 414	. . . . . . . 8 ⊢ (F Fn A → (((xFz ∧ yFz) → x = y) ↔ ((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) → x = y))))
32	31	bialdv 935	. . . . . . 7 ⊢ (F Fn A → (∀z((xFz ∧ yFz) → x = y) ↔ ∀z((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) → x = y))))
33		19.21v 942	. . . . . . . 8 ⊢ (∀z((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) → x = y)) ↔ ((x ∈ A ∧ y ∈ A) → ∀z((z = (F ‘x) ∧ z = (F ‘y)) → x = y)))
34		19.23v 950	. . . . . . . . . 10 ⊢ (∀z((z = (F ‘x) ∧ z = (F ‘y)) → x = y) ↔ (∃z(z = (F ‘x) ∧ z = (F ‘y)) → x = y))
35		fvex 2838	. . . . . . . . . . . 12 ⊢ (F ‘x) ∈ V
36	35	eqvinc 1407	. . . . . . . . . . 11 ⊢ ((F ‘x) = (F ‘y) ↔ ∃z(z = (F ‘x) ∧ z = (F ‘y)))
37	36	imbi1i 161	. . . . . . . . . 10 ⊢ (((F ‘x) = (F ‘y) → x = y) ↔ (∃z(z = (F ‘x) ∧ z = (F ‘y)) → x = y))
38	34, 37	bitr4 154	. . . . . . . . 9 ⊢ (∀z((z = (F ‘x) ∧ z = (F ‘y)) → x = y) ↔ ((F ‘x) = (F ‘y) → x = y))
39	38	imbi2i 160	. . . . . . . 8 ⊢ (((x ∈ A ∧ y ∈ A) → ∀z((z = (F ‘x) ∧ z = (F ‘y)) → x = y)) ↔ ((x ∈ A ∧ y ∈ A) → ((F ‘x) = (F ‘y) → x = y)))
40	33, 39	bitr 151	. . . . . . 7 ⊢ (∀z((x ∈ A ∧ y ∈ A) → ((z = (F ‘x) ∧ z = (F ‘y)) → x = y)) ↔ ((x ∈ A ∧ y ∈ A) → ((F ‘x) = (F ‘y) → x = y)))
41	32, 40	syl6bb 414	. . . . . 6 ⊢ (F Fn A → (∀z((xFz ∧ yFz) → x = y) ↔ ((x ∈ A ∧ y ∈ A) → ((F ‘x) = (F ‘y) → x = y))))
42	41	bi2aldv 937	. . . . 5 ⊢ (F Fn A → (∀x∀y∀z((xFz ∧ yFz) → x = y) ↔ ∀x∀y((x ∈ A ∧ y ∈ A) → ((F ‘x) = (F ‘y) → x = y))))
43		breq1 2065	. . . . . . . 8 ⊢ (x = y → (xFz ↔ yFz))
44	43	mo4 1029	. . . . . . 7 ⊢ (∃*x xFz ↔ ∀x∀y((xFz ∧ yFz) → x = y))
45	44	bial 695	. . . . . 6 ⊢ (∀z∃*x xFz ↔ ∀z∀x∀y((xFz ∧ yFz) → x = y))
46		alcom 715	. . . . . 6 ⊢ (∀z∀x∀y((xFz ∧ yFz) → x = y) ↔ ∀x∀z∀y((xFz ∧ yFz) → x = y))
47		alcom 715	. . . . . . 7 ⊢ (∀z∀y((xFz ∧ yFz) → x = y) ↔ ∀y∀z((xFz ∧ yFz) → x = y))
48	47	bial 695	. . . . . 6 ⊢ (∀x∀z∀y((xFz ∧ yFz) → x = y) ↔ ∀x∀y∀z((xFz ∧ yFz) → x = y))
49	45, 46, 48	3bitr 155	. . . . 5 ⊢ (∀z∃*x xFz ↔ ∀x∀y∀z((xFz ∧ yFz) → x = y))
50		r2al 1231	. . . . 5 ⊢ (∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y) ↔ ∀x∀y((x ∈ A ∧ y ∈ A) → ((F ‘x) = (F ‘y) → x = y)))
51	42, 49, 50	3bitr4g 428	. . . 4 ⊢ (F Fn A → (∀z∃*x xFz ↔ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))
52	2, 51	syl 12	. . 3 ⊢ (F:A–→B → (∀z∃*x xFz ↔ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))
53	52	pm5.32i 489	. 2 ⊢ ((F:A–→B ∧ ∀z∃*x xFz) ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))
54	1, 53	bitr 151	1 ⊢ (F:A–1-1→B ↔ (F:A–→B ∧ ∀x ∈ A ∀y ∈ A ((F ‘x) = (F ‘y) → x = y)))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672  ∃wex 678   = weq 797  ∃*wmo 1008   = wceq 1091   ∈ wcel 1092  ∀wral 1201   class class class wbr 2054  dom cdm 2410   Fn wfn 2417  –→wf 2418  –1-1→wf1 2419   ‘cfv 2422

This theorem is referenced by:  f1fvf 2917  f1fveq 2918  tz7.48lem 2993  omsmo 3196  mapenlem2 3385  unfilem2 3439  inf3lem6 3469  alephiso 3697  om2uzf1o 4656

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-un 1076  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-ral 1205  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-uni 1920  df-br 2063  df-opab 2098  df-id 2125  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438

metamath.org