Theorem f1mpt 7265

Description: Express injection for a mapping operation. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
f1mpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
f1mpt.2	⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)

Assertion

Ref	Expression
f1mpt	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑦,𝐶   𝑥,𝐷   𝑦,𝐹

Allowed substitution hints:   𝐶(𝑥)   𝐷(𝑦)   𝐹(𝑥)

Proof of Theorem f1mpt

Step	Hyp	Ref	Expression
1		f1mpt.1	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
2		nfmpt1 5203	. . . 4 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
3	1, 2	nfcxfr 2920	. . 3 ⊢ Ⅎ𝑥𝐹
4		nfcv 2922	. . 3 ⊢ Ⅎ𝑦𝐹
5	3, 4	dff13f 7259	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
6	1	fmpt 7110	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
7	6	anbi1i 636	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
8		f1mpt.2	. . . . . . 7 ⊢ (𝑥 = 𝑦 → 𝐶 = 𝐷)
9	8	eleq1d 2845	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝐶 ∈ 𝐵 ↔ 𝐷 ∈ 𝐵))
10	9	cbvralvw 3240	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐴 𝐷 ∈ 𝐵)
11		raaanv 4474	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐴 𝐷 ∈ 𝐵))
12	1	fvmpt2 7005	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) → (𝐹‘𝑥) = 𝐶)
13	8, 1	fvmptg 6991	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐹‘𝑦) = 𝐷)
14	12, 13	eqeqan12d 2774	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝐶 = 𝐷))
15	14	an4s 673	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ 𝐶 = 𝐷))
16	15	imbi1d 344	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (𝐶 = 𝐷 → 𝑥 = 𝑦)))
17	16	ex 418	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (𝐶 = 𝐷 → 𝑥 = 𝑦))))
18	17	ralimdva 3174	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → ∀𝑦 ∈ 𝐴 (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (𝐶 = 𝐷 → 𝑥 = 𝑦))))
19		ralbi 3117	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ (𝐶 = 𝐷 → 𝑥 = 𝑦)) → (∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
20	18, 19	syl6 36	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦))))
21	20	ralimia 3096	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
22		ralbi 3117	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
23	21, 22	syl 18	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
24	11, 23	sylbir 238	. . . . 5 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐴 𝐷 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
25	10, 24	sylan2b 606	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
26	25	anidms 577	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
27	26	pm5.32i 585	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)) ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))
28	5, 7, 27	3bitr2i 302	1 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝐶 = 𝐷 → 𝑥 = 𝑦)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ↦ cmpt 5185  ⟶wf 6534  –1-1→wf1 6535  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fv 6546

This theorem is used by:  ismon2  17914  isepi2  17921  chninf  18814  uspgredg2v  29810  usgredg2v  29813  aciunf1lem  33303  fnpreimac  33311  rlocf1  33881  zringfrac  34132  selvply1rhmlema  34196  selvply1rhmlem1  34198  ply1degltdimlem  34300  ply1degltdim  34301  assalactf1o  34313  soinfdom  35768  mh-inf3sn  37422  disjf1  46291  upgrimtrls  49097