Theorem f1ompt 5741

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 5432	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		dff1o4 5539	. . . . . 6 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
3	2	baib 921	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
4	1, 3	syl 14	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
5		fnres 5399	. . . . . 6 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧)
6		nfcv 2349	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑧
7		fmpt.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
8		nfmpt1 4142	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
9	7, 8	nfcxfr 2346	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝐹
10		nfcv 2349	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑦
11	6, 9, 10	nfbr 4095	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧𝐹𝑦
12		nfv 1552	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)
13		breq1 4051	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦))
14		df-mpt 4112	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
15	7, 14	eqtri 2227	. . . . . . . . . . . 12 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
16	15	breqi 4054	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑦 ↔ 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦)
17		df-br 4049	. . . . . . . . . . . 12 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)})
18		opabid 4307	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
19	17, 18	bitri 184	. . . . . . . . . . 11 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
20	16, 19	bitri 184	. . . . . . . . . 10 ⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
21	13, 20	bitrdi 196	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)))
22	11, 12, 21	cbveu 2079	. . . . . . . 8 ⊢ (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
23		vex 2776	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
24		vex 2776	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
25	23, 24	brcnv 4866	. . . . . . . . 9 ⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦)
26	25	eubii 2064	. . . . . . . 8 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27		df-reu 2492	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
28	22, 26, 27	3bitr4i 212	. . . . . . 7 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
29	28	ralbii 2513	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
30	5, 29	bitri 184	. . . . 5 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
31		relcnv 5066	. . . . . . 7 ⊢ Rel ◡𝐹
32		df-rn 4691	. . . . . . . 8 ⊢ ran 𝐹 = dom ◡𝐹
33		frn 5441	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
34	32, 33	eqsstrrid 3242	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵)
35		relssres 5003	. . . . . . 7 ⊢ ((Rel ◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹)
36	31, 34, 35	sylancr 414	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹)
37	36	fneq1d 5370	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ◡𝐹 Fn 𝐵))
38	30, 37	bitr3id 194	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡𝐹 Fn 𝐵))
39	4, 38	bitr4d 191	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
40	39	pm5.32i 454	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
41		f1of 5531	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
42	41	pm4.71ri 392	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵))
43	7	fmpt 5740	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
44	43	anbi1i 458	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
45	40, 42, 44	3bitr4i 212	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1373  ∃!weu 2055   ∈ wcel 2177  ∀wral 2485  ∃!wreu 2487   ⊆ wss 3168  ⟨cop 3638   class class class wbr 4048  {copab 4109   ↦ cmpt 4110  ^◡ccnv 4679  dom cdm 4680  ran crn 4681   ↾ cres 4682  Rel wrel 4685   Fn wfn 5272  ⟶wf 5273  –1-1-onto→wf1o 5276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4167  ax-pow 4223  ax-pr 4258

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-reu 2492  df-rab 2494  df-v 2775  df-sbc 3001  df-un 3172  df-in 3174  df-ss 3181  df-pw 3620  df-sn 3641  df-pr 3642  df-op 3644  df-uni 3854  df-br 4049  df-opab 4111  df-mpt 4112  df-id 4345  df-xp 4686  df-rel 4687  df-cnv 4688  df-co 4689  df-dm 4690  df-rn 4691  df-res 4692  df-ima 4693  df-iota 5238  df-fun 5279  df-fn 5280  df-f 5281  df-f1 5282  df-fo 5283  df-f1o 5284  df-fv 5285

This theorem is referenced by:  xpf1o  6953  icoshftf1o  10126