Theorem f1ompt 5853

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 5531	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		dff1o4 5645	. . . . . 6 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵))
3	2	baib 931	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
4	1, 3	syl 14	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹 Fn 𝐵))
5		fnres 5498	. . . . . 6 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧)
6		nfcv 2392	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑧
7		fmpt.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)
8		nfmpt1 4222	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐶)
9	7, 8	nfcxfr 2389	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝐹
10		nfcv 2392	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝑦
11	6, 9, 10	nfbr 4175	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧𝐹𝑦
12		nfv 1581	. . . . . . . . 9 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)
13		breq1 4131	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ 𝑥𝐹𝑦))
14		df-mpt 4192	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
15	7, 14	eqtri 2259	. . . . . . . . . . . 12 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}
16	15	breqi 4134	. . . . . . . . . . 11 ⊢ (𝑥𝐹𝑦 ↔ 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦)
17		df-br 4129	. . . . . . . . . . . 12 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)})
18		opabid 4396	. . . . . . . . . . . 12 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)} ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
19	17, 18	bitri 184	. . . . . . . . . . 11 ⊢ (𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)}𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
20	16, 19	bitri 184	. . . . . . . . . 10 ⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
21	13, 20	bitrdi 196	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝑧𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶)))
22	11, 12, 21	cbveu 2110	. . . . . . . 8 ⊢ (∃!𝑧 𝑧𝐹𝑦 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
23		vex 2824	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
24		vex 2824	. . . . . . . . . 10 ⊢ 𝑧 ∈ V
25	23, 24	brcnv 4961	. . . . . . . . 9 ⊢ (𝑦◡𝐹𝑧 ↔ 𝑧𝐹𝑦)
26	25	eubii 2095	. . . . . . . 8 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑧 𝑧𝐹𝑦)
27		df-reu 2535	. . . . . . . 8 ⊢ (∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶))
28	22, 26, 27	3bitr4i 212	. . . . . . 7 ⊢ (∃!𝑧 𝑦◡𝐹𝑧 ↔ ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
29	28	ralbii 2556	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐵 ∃!𝑧 𝑦◡𝐹𝑧 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
30	5, 29	bitri 184	. . . . 5 ⊢ ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶)
31		relcnv 5163	. . . . . . 7 ⊢ Rel ◡𝐹
32		df-rn 4783	. . . . . . . 8 ⊢ ran 𝐹 = dom ◡𝐹
33		frn 5540	. . . . . . . 8 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
34	32, 33	eqsstrrid 3295	. . . . . . 7 ⊢ (𝐹:𝐴⟶𝐵 → dom ◡𝐹 ⊆ 𝐵)
35		relssres 5099	. . . . . . 7 ⊢ ((Rel ◡𝐹 ∧ dom ◡𝐹 ⊆ 𝐵) → (◡𝐹 ↾ 𝐵) = ◡𝐹)
36	31, 34, 35	sylancr 418	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 ↾ 𝐵) = ◡𝐹)
37	36	fneq1d 5469	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → ((◡𝐹 ↾ 𝐵) Fn 𝐵 ↔ ◡𝐹 Fn 𝐵))
38	30, 37	bitr3id 194	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶 ↔ ◡𝐹 Fn 𝐵))
39	4, 38	bitr4d 191	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
40	39	pm5.32i 458	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
41		f1of 5637	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
42	41	pm4.71ri 396	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ 𝐹:𝐴–1-1-onto→𝐵))
43	7	fmpt 5852	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵)
44	43	anbi1i 462	. 2 ⊢ ((∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))
45	40, 42, 44	3bitr4i 212	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃!𝑥 ∈ 𝐴 𝑦 = 𝐶))

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1402  ∃!weu 2086   ∈ wcel 2209  ∀wral 2528  ∃!wreu 2530   ⊆ wss 3220  ⟨cop 3711   class class class wbr 4128  {copab 4189   ↦ cmpt 4190  ^◡ccnv 4771  dom cdm 4772  ran crn 4773   ↾ cres 4774  Rel wrel 4777   Fn wfn 5370  ⟶wf 5371  –1-1-onto→wf1o 5374

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4247  ax-pow 4309  ax-pr 4344

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-opab 4191  df-mpt 4192  df-id 4436  df-xp 4778  df-rel 4779  df-cnv 4780  df-co 4781  df-dm 4782  df-rn 4783  df-res 4784  df-ima 4785  df-iota 5335  df-fun 5377  df-fn 5378  df-f 5379  df-f1 5380  df-fo 5381  df-f1o 5382  df-fv 5383

This theorem is referenced by:  xpf1o  7138  icoshftf1o  10376