Theorem f1ompt 5263

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	|- F = (x e. A |-> C)

Assertion

Ref	Expression
f1ompt	|- ( F :A -1-1-onto->B <-> (A.x e. A C e. B /\ A.y e. B E!x e. A y = C))

Distinct variable groups:   x,y,A   x,B,y   y, C   y, F

Allowed substitution hints:   C(x)   F(x)

Proof of Theorem f1ompt

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffn 4989	. . . . 5 |- ( F :A -->B -> F Fn A)
2		dff1o4 5077	. . . . . 6 |- ( F :A -1-1-onto->B <-> ( F Fn A /\ `' F Fn B))
3	2	baib 827	. . . . 5 |- ( F Fn A -> ( F :A -1-1-onto->B <-> `' F Fn B))
4	1, 3	syl 14	. . . 4 |- ( F :A -->B -> ( F :A -1-1-onto->B <-> `' F Fn B))
5		fnres 4958	. . . . . 6 |- (( `' F |` B) Fn B <-> A.y e. B E!z y `' Fz)
6		nfcv 2175	. . . . . . . . . 10 |- F/_xz
7		fmpt.1	. . . . . . . . . . 11 |- F = (x e. A |-> C)
8		nfmpt1 3841	. . . . . . . . . . 11 |- F/_x(x e. A |-> C)
9	7, 8	nfcxfr 2172	. . . . . . . . . 10 |- F/_x F
10		nfcv 2175	. . . . . . . . . 10 |- F/_xy
11	6, 9, 10	nfbr 3799	. . . . . . . . 9 |- F/x z Fy
12		nfv 1418	. . . . . . . . 9 |- F/z(x e. A /\ y = C)
13		breq1 3758	. . . . . . . . . 10 |- (z = x -> (z Fy <-> x Fy))
14		df-mpt 3811	. . . . . . . . . . . . 13 |- (x e. A |-> C) = { <.x , y >. | (x e. A /\ y = C) }
15	7, 14	eqtri 2057	. . . . . . . . . . . 12 |- F = { <.x , y >. | (x e. A /\ y = C) }
16	15	breqi 3761	. . . . . . . . . . 11 |- (x Fy <-> x { <.x , y >. | (x e. A /\ y = C) }y)
17		df-br 3756	. . . . . . . . . . . 12 |- (x { <.x , y >. | (x e. A /\ y = C) }y <-> <.x , y >. e. { <.x , y >. | (x e. A /\ y = C) })
18		opabid 3985	. . . . . . . . . . . 12 |- ( <.x , y >. e. { <.x , y >. | (x e. A /\ y = C) } <-> (x e. A /\ y = C))
19	17, 18	bitri 173	. . . . . . . . . . 11 |- (x { <.x , y >. | (x e. A /\ y = C) }y <-> (x e. A /\ y = C))
20	16, 19	bitri 173	. . . . . . . . . 10 |- (x Fy <-> (x e. A /\ y = C))
21	13, 20	syl6bb 185	. . . . . . . . 9 |- (z = x -> (z Fy <-> (x e. A /\ y = C)))
22	11, 12, 21	cbveu 1921	. . . . . . . 8 |- (E!z z Fy <-> E!x(x e. A /\ y = C))
23		vex 2554	. . . . . . . . . 10 |- y e. _V
24		vex 2554	. . . . . . . . . 10 |- z e. _V
25	23, 24	brcnv 4461	. . . . . . . . 9 |- (y `' Fz <-> z Fy)
26	25	eubii 1906	. . . . . . . 8 |- (E!z y `' Fz <-> E!z z Fy)
27		df-reu 2307	. . . . . . . 8 |- (E!x e. A y = C <-> E!x(x e. A /\ y = C))
28	22, 26, 27	3bitr4i 201	. . . . . . 7 |- (E!z y `' Fz <-> E!x e. A y = C)
29	28	ralbii 2324	. . . . . 6 |- (A.y e. B E!z y `' Fz <-> A.y e. B E!x e. A y = C)
30	5, 29	bitri 173	. . . . 5 |- (( `' F |` B) Fn B <-> A.y e. B E!x e. A y = C)
31		relcnv 4646	. . . . . . 7 |- Rel `' F
32		df-rn 4299	. . . . . . . 8 |- ran F = dom `' F
33		frn 4995	. . . . . . . 8 |- ( F :A -->B -> ran F C_ B)
34	32, 33	syl5eqssr 2984	. . . . . . 7 |- ( F :A -->B -> dom `' F C_ B)
35		relssres 4591	. . . . . . 7 |- (( Rel `' F /\ dom `' F C_ B) -> ( `' F |` B) = `' F)
36	31, 34, 35	sylancr 393	. . . . . 6 |- ( F :A -->B -> ( `' F |` B) = `' F)
37	36	fneq1d 4932	. . . . 5 |- ( F :A -->B -> (( `' F |` B) Fn B <-> `' F Fn B))
38	30, 37	syl5bbr 183	. . . 4 |- ( F :A -->B -> (A.y e. B E!x e. A y = C <-> `' F Fn B))
39	4, 38	bitr4d 180	. . 3 |- ( F :A -->B -> ( F :A -1-1-onto->B <-> A.y e. B E!x e. A y = C))
40	39	pm5.32i 427	. 2 |- (( F :A -->B /\ F :A -1-1-onto->B) <-> ( F :A -->B /\ A.y e. B E!x e. A y = C))
41		f1of 5069	. . 3 |- ( F :A -1-1-onto->B -> F :A -->B)
42	41	pm4.71ri 372	. 2 |- ( F :A -1-1-onto->B <-> ( F :A -->B /\ F :A -1-1-onto->B))
43	7	fmpt 5262	. . 3 |- (A.x e. A C e. B <-> F :A -->B)
44	43	anbi1i 431	. 2 |- ((A.x e. A C e. B /\ A.y e. B E!x e. A y = C) <-> ( F :A -->B /\ A.y e. B E!x e. A y = C))
45	40, 42, 44	3bitr4i 201	1 |- ( F :A -1-1-onto->B <-> (A.x e. A C e. B /\ A.y e. B E!x e. A y = C))

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1242   e. wcel 1390  E!weu 1897  A.wral 2300  E!wreu 2302   C_ wss 2911   <.cop 3370   class class class wbr 3755   {copab 3808   |-> cmpt 3809   `'ccnv 4287   dom cdm 4288   ran crn 4289   |` cres 4290   Rel wrel 4293   Fn wfn 4840   -->wf 4841   -1-1-onto->wf1o 4844

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-rab 2309  df-v 2553  df-sbc 2759  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-res 4300  df-ima 4301  df-iota 4810  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-fv 4853

This theorem is referenced by:  icoshftf1o  8629