Theorem f1ompt 7083

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 6688	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		dff1o4 6808	. . . . . 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 6645	. . . . . 6 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧)
6		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑧
7		fmpt.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
8		nfmpt1 5206	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
9	7, 8	nfcxfr 2889	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝐹
10		nfcv 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑦
11	6, 9, 10	nfbr 5154	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧𝐹𝑦
12		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)
13		breq1 5110	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦))
14		df-mpt 5189	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
15	7, 14	eqtri 2752	. . . . . . . . . . . 12 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
16	15	breqi 5113	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑦 ↔ 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦)
17		df-br 5108	. . . . . . . . . . . 12 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)})
18		opabidw 5484	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
19	17, 18	bitri 275	. . . . . . . . . . 11 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
20	16, 19	bitri 275	. . . . . . . . . 10 ⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
21	13, 20	bitrdi 287	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)))
22	11, 12, 21	cbveuw 2599	. . . . . . . 8 ⊢ (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
23		vex 3451	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
24		vex 3451	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
25	23, 24	brcnv 5846	. . . . . . . . 9 ⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦)
26	25	eubii 2578	. . . . . . . 8 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27		df-reu 3355	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
28	22, 26, 27	3bitr4i 303	. . . . . . 7 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
29	28	ralbii 3075	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
30	5, 29	bitri 275	. . . . 5 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
31		relcnv 6075	. . . . . . 7 ⊢ Rel ◡𝐹
32		df-rn 5649	. . . . . . . 8 ⊢ ran 𝐹 = dom ◡𝐹
33		frn 6695	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
34	32, 33	eqsstrrid 3986	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵)
35		relssres 5993	. . . . . . 7 ⊢ ((Rel ◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹)
36	31, 34, 35	sylancr 587	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹)
37	36	fneq1d 6611	. . . . 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 6800	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
42	41	pm4.71ri 560	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵))
43	7	fmpt 7082	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
44	43	anbi1i 624	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
45	40, 42, 44	3bitr4i 303	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!weu 2561  ∀wral 3044  ∃!wreu 3352   ⊆ wss 3914  ⟨cop 4595   class class class wbr 5107  {copab 5169   ↦ cmpt 5188  ^◡ccnv 5637  dom cdm 5638  ran crn 5639   ↾ cres 5640  Rel wrel 5643   Fn wfn 6506  ⟶wf 6507  –1-1-onto→wf1o 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  oaf1o  8527  xpf1o  9103  icoshftf1o  13435  fprodser  15915  dfod2  19494  gsummptf1o  19893  nbusgrf1o0  29296  cusgrfilem2  29384  numclwlk2lem2f1o  30308  f1mptrn  32559  ccatws1f1o  32873  gsummptfsf1o  32994  xrmulc1cn  33920  poimirlem4  37618  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  isuspgrim0lem  47893  isuspgrim0  47894  isuspgrimlem  47895