Theorem f1ompt 7057

Description: Express bijection for a mapping operation. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by Mario Carneiro, 4-Dec-2016.)

Hypothesis

Ref	Expression
fmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)

Assertion

Ref	Expression
f1ompt	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))

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

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

Proof of Theorem f1ompt

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 6662	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		dff1o4 6782	. . . . . 6 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
3	2	baib 535	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
4	1, 3	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
5		fnres 6619	. . . . . 6 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧)
6		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑧
7		fmpt.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
8		nfmpt1 5185	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
9	7, 8	nfcxfr 2897	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝐹
10		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑦
11	6, 9, 10	nfbr 5133	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧𝐹𝑦
12		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)
13		breq1 5089	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦))
14		df-mpt 5168	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
15	7, 14	eqtri 2760	. . . . . . . . . . . 12 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
16	15	breqi 5092	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑦 ↔ 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦)
17		df-br 5087	. . . . . . . . . . . 12 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)})
18		opabidw 5472	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
19	17, 18	bitri 275	. . . . . . . . . . 11 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
20	16, 19	bitri 275	. . . . . . . . . 10 ⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
21	13, 20	bitrdi 287	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)))
22	11, 12, 21	cbveuw 2607	. . . . . . . 8 ⊢ (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
23		vex 3434	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
24		vex 3434	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
25	23, 24	brcnv 5831	. . . . . . . . 9 ⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦)
26	25	eubii 2586	. . . . . . . 8 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27		df-reu 3344	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
28	22, 26, 27	3bitr4i 303	. . . . . . 7 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
29	28	ralbii 3084	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
30	5, 29	bitri 275	. . . . 5 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
31		relcnv 6063	. . . . . . 7 ⊢ Rel ◡𝐹
32		df-rn 5635	. . . . . . . 8 ⊢ ran 𝐹 = dom ◡𝐹
33		frn 6669	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
34	32, 33	eqsstrrid 3962	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵)
35		relssres 5981	. . . . . . 7 ⊢ ((Rel ◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹)
36	31, 34, 35	sylancr 588	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹)
37	36	fneq1d 6585	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ◡𝐹 Fn 𝐵))
38	30, 37	bitr3id 285	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡𝐹 Fn 𝐵))
39	4, 38	bitr4d 282	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
40	39	pm5.32i 574	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
41		f1of 6774	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
42	41	pm4.71ri 560	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵))
43	7	fmpt 7056	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
44	43	anbi1i 625	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
45	40, 42, 44	3bitr4i 303	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!weu 2569  ∀wral 3052  ∃!wreu 3341   ⊆ wss 3890  ⟨cop 4574   class class class wbr 5086  {copab 5148   ↦ cmpt 5167  ^◡ccnv 5623  dom cdm 5624  ran crn 5625   ↾ cres 5626  Rel wrel 5629   Fn wfn 6487  ⟶wf 6488  –1-1-onto→wf1o 6491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  oaf1o  8491  xpf1o  9070  icoshftf1o  13418  fprodser  15905  dfod2  19530  gsummptf1o  19929  nbusgrf1o0  29452  cusgrfilem2  29540  numclwlk2lem2f1o  30464  f1mptrn  32723  ccatws1f1o  33026  gsummptf1od  33131  gsummptfsf1o  33136  xrmulc1cn  34090  poimirlem4  37959  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  isuspgrim0lem  48381  isuspgrim0  48382  isuspgrimlem  48383