Theorem foimacnv 5772

Description: A reverse version of f1imacnv 5771. (Contributed by Jeff Hankins, 16-Jul-2009.)

Assertion

Ref	Expression
foimacnv	|- ( ( F : A -onto-> B /\ C C_ B ) -> ( F " ( `' F " C ) ) = C )

Proof of Theorem foimacnv

Step	Hyp	Ref	Expression
1		resima 5247	. 2 |- ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) = ( F " ( `' F " C ) )
2		fofun 5735	. . . . . 6 |- ( F : A -onto-> B -> Fun F )
3	2	adantr 463	. . . . 5 |- ( ( F : A -onto-> B /\ C C_ B ) -> Fun F )
4		funcnvres2 5596	. . . . 5 |- ( Fun F -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
5	3, 4	syl 17	. . . 4 |- ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) = ( F |` ( `' F " C ) ) )
6	5	imaeq1d 5277	. . 3 |- ( ( F : A -onto-> B /\ C C_ B ) -> ( `' ( `' F |` C ) " ( `' F " C ) ) = ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) )
7		resss 5238	. . . . . . . . . . 11 |- ( `' F |` C ) C_ `' F
8		cnvss 5117	. . . . . . . . . . 11 |- ( ( `' F |` C ) C_ `' F -> `' ( `' F |` C ) C_ `' `' F )
9	7, 8	ax-mp 5	. . . . . . . . . 10 |- `' ( `' F |` C ) C_ `' `' F
10		cnvcnvss 5399	. . . . . . . . . 10 |- `' `' F C_ F
11	9, 10	sstri 3450	. . . . . . . . 9 |- `' ( `' F |` C ) C_ F
12		funss 5543	. . . . . . . . 9 |- ( `' ( `' F |` C ) C_ F -> ( Fun F -> Fun `' ( `' F |` C ) ) )
13	11, 2, 12	mpsyl 62	. . . . . . . 8 |- ( F : A -onto-> B -> Fun `' ( `' F |` C ) )
14	13	adantr 463	. . . . . . 7 |- ( ( F : A -onto-> B /\ C C_ B ) -> Fun `' ( `' F |` C ) )
15		df-ima 4955	. . . . . . . 8 |- ( `' F " C ) = ran ( `' F |` C )
16		df-rn 4953	. . . . . . . 8 |- ran ( `' F |` C ) = dom `' ( `' F |` C )
17	15, 16	eqtr2i 2432	. . . . . . 7 |- dom `' ( `' F |` C ) = ( `' F " C )
18	14, 17	jctir 536	. . . . . 6 |- ( ( F : A -onto-> B /\ C C_ B ) -> ( Fun `' ( `' F |` C ) /\ dom `' ( `' F |` C ) = ( `' F " C ) ) )
19		df-fn 5528	. . . . . 6 |- ( `' ( `' F |` C ) Fn ( `' F " C ) <-> ( Fun `' ( `' F |` C ) /\ dom `' ( `' F |` C ) = ( `' F " C ) ) )
20	18, 19	sylibr 212	. . . . 5 |- ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) Fn ( `' F " C ) )
21		dfdm4 5137	. . . . . 6 |- dom ( `' F |` C ) = ran `' ( `' F |` C )
22		forn 5737	. . . . . . . . . 10 |- ( F : A -onto-> B -> ran F = B )
23	22	sseq2d 3469	. . . . . . . . 9 |- ( F : A -onto-> B -> ( C C_ ran F <-> C C_ B ) )
24	23	biimpar 483	. . . . . . . 8 |- ( ( F : A -onto-> B /\ C C_ B ) -> C C_ ran F )
25		df-rn 4953	. . . . . . . 8 |- ran F = dom `' F
26	24, 25	syl6sseq 3487	. . . . . . 7 |- ( ( F : A -onto-> B /\ C C_ B ) -> C C_ dom `' F )
27		ssdmres 5236	. . . . . . 7 |- ( C C_ dom `' F <-> dom ( `' F |` C ) = C )
28	26, 27	sylib 196	. . . . . 6 |- ( ( F : A -onto-> B /\ C C_ B ) -> dom ( `' F |` C ) = C )
29	21, 28	syl5eqr 2457	. . . . 5 |- ( ( F : A -onto-> B /\ C C_ B ) -> ran `' ( `' F |` C ) = C )
30		df-fo 5531	. . . . 5 |- ( `' ( `' F |` C ) : ( `' F " C ) -onto-> C <-> ( `' ( `' F |` C ) Fn ( `' F " C ) /\ ran `' ( `' F |` C ) = C ) )
31	20, 29, 30	sylanbrc 662	. . . 4 |- ( ( F : A -onto-> B /\ C C_ B ) -> `' ( `' F |` C ) : ( `' F " C ) -onto-> C )
32		foima 5739	. . . 4 |- ( `' ( `' F |` C ) : ( `' F " C ) -onto-> C -> ( `' ( `' F |` C ) " ( `' F " C ) ) = C )
33	31, 32	syl 17	. . 3 |- ( ( F : A -onto-> B /\ C C_ B ) -> ( `' ( `' F |` C ) " ( `' F " C ) ) = C )
34	6, 33	eqtr3d 2445	. 2 |- ( ( F : A -onto-> B /\ C C_ B ) -> ( ( F |` ( `' F " C ) ) " ( `' F " C ) ) = C )
35	1, 34	syl5eqr 2457	1 |- ( ( F : A -onto-> B /\ C C_ B ) -> ( F " ( `' F " C ) ) = C )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1405   C_ wss 3413   `'ccnv 4941   dom cdm 4942   ran crn 4943   |` cres 4944   "cima 4945   Fun wfun 5519   Fn wfn 5520   -onto->wfo 5523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-id 4737  df-xp 4948  df-rel 4949  df-cnv 4950  df-co 4951  df-dm 4952  df-rn 4953  df-res 4954  df-ima 4955  df-fun 5527  df-fn 5528  df-f 5529  df-fo 5531

This theorem is referenced by:  f1opw2  6465  imacosupp  6897  fopwdom  7583  f1opwfi  7778  enfin2i  8653  fin1a2lem7  8738  fsumss  13603  fprodss  13814  gicsubgen  16542  gsumval3OLD  17124  coe1mul2lem2  18521  cncmp  20077  cnconn  20107  qtoprest  20402  qtopomap  20403  qtopcmap  20404  hmeoimaf1o  20455  elfm3  20635  imasf1oxms  21176  mbfimaopnlem  22246  cvmsss2  29452  diaintclN  34059  dibintclN  34168  dihintcl  34345  lnmepi  35374  pwfi2f1o  35387  pwfi2f1oOLD  35388