Theorem foimacnv 6801

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

Assertion

Ref	Expression
foimacnv	⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)

Proof of Theorem foimacnv

Step	Hyp	Ref	Expression
1		resima 5984	. 2 ⊢ ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = (𝐹 “ (◡𝐹 “ 𝐶))
2		fofun 6757	. . . . . 6 ⊢ (𝐹:𝐴–onto→𝐵 → Fun 𝐹)
3	2	adantr 480	. . . . 5 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun 𝐹)
4		funcnvres2 6582	. . . . 5 ⊢ (Fun 𝐹 → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶)))
5	3, 4	syl 17	. . . 4 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) = (𝐹 ↾ (◡𝐹 “ 𝐶)))
6	5	imaeq1d 6028	. . 3 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)))
7		resss 5970	. . . . . . . . . 10 ⊢ (◡𝐹 ↾ 𝐶) ⊆ ◡𝐹
8		cnvss 5831	. . . . . . . . . 10 ⊢ ((◡𝐹 ↾ 𝐶) ⊆ ◡𝐹 → ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹)
9	7, 8	ax-mp 5	. . . . . . . . 9 ⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ ◡◡𝐹
10		cnvcnvss 6162	. . . . . . . . 9 ⊢ ◡◡𝐹 ⊆ 𝐹
11	9, 10	sstri 3945	. . . . . . . 8 ⊢ ◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹
12		funss 6521	. . . . . . . 8 ⊢ (◡(◡𝐹 ↾ 𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun ◡(◡𝐹 ↾ 𝐶)))
13	11, 2, 12	mpsyl 68	. . . . . . 7 ⊢ (𝐹:𝐴–onto→𝐵 → Fun ◡(◡𝐹 ↾ 𝐶))
14	13	adantr 480	. . . . . 6 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → Fun ◡(◡𝐹 ↾ 𝐶))
15		df-ima 5647	. . . . . . 7 ⊢ (◡𝐹 “ 𝐶) = ran (◡𝐹 ↾ 𝐶)
16		df-rn 5645	. . . . . . 7 ⊢ ran (◡𝐹 ↾ 𝐶) = dom ◡(◡𝐹 ↾ 𝐶)
17	15, 16	eqtr2i 2761	. . . . . 6 ⊢ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶)
18		df-fn 6505	. . . . . 6 ⊢ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ↔ (Fun ◡(◡𝐹 ↾ 𝐶) ∧ dom ◡(◡𝐹 ↾ 𝐶) = (◡𝐹 “ 𝐶)))
19	14, 17, 18	sylanblrc 591	. . . . 5 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶))
20		dfdm4 5854	. . . . . 6 ⊢ dom (◡𝐹 ↾ 𝐶) = ran ◡(◡𝐹 ↾ 𝐶)
21		forn 6759	. . . . . . . . . 10 ⊢ (𝐹:𝐴–onto→𝐵 → ran 𝐹 = 𝐵)
22	21	sseq2d 3968	. . . . . . . . 9 ⊢ (𝐹:𝐴–onto→𝐵 → (𝐶 ⊆ ran 𝐹 ↔ 𝐶 ⊆ 𝐵))
23	22	biimpar 477	. . . . . . . 8 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ ran 𝐹)
24		df-rn 5645	. . . . . . . 8 ⊢ ran 𝐹 = dom ◡𝐹
25	23, 24	sseqtrdi 3976	. . . . . . 7 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → 𝐶 ⊆ dom ◡𝐹)
26		ssdmres 5982	. . . . . . 7 ⊢ (𝐶 ⊆ dom ◡𝐹 ↔ dom (◡𝐹 ↾ 𝐶) = 𝐶)
27	25, 26	sylib 218	. . . . . 6 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → dom (◡𝐹 ↾ 𝐶) = 𝐶)
28	20, 27	eqtr3id 2786	. . . . 5 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ran ◡(◡𝐹 ↾ 𝐶) = 𝐶)
29		df-fo 6508	. . . . 5 ⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 ↔ (◡(◡𝐹 ↾ 𝐶) Fn (◡𝐹 “ 𝐶) ∧ ran ◡(◡𝐹 ↾ 𝐶) = 𝐶))
30	19, 28, 29	sylanbrc 584	. . . 4 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶)
31		foima 6761	. . . 4 ⊢ (◡(◡𝐹 ↾ 𝐶):(◡𝐹 “ 𝐶)–onto→𝐶 → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶)
32	30, 31	syl 17	. . 3 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (◡(◡𝐹 ↾ 𝐶) “ (◡𝐹 “ 𝐶)) = 𝐶)
33	6, 32	eqtr3d 2774	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → ((𝐹 ↾ (◡𝐹 “ 𝐶)) “ (◡𝐹 “ 𝐶)) = 𝐶)
34	1, 33	eqtr3id 2786	1 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝐶 ⊆ 𝐵) → (𝐹 “ (◡𝐹 “ 𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ^◡ccnv 5633  dom cdm 5634  ran crn 5635   ↾ cres 5636   “ cima 5637  Fun wfun 6496   Fn wfn 6497  –onto→wfo 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-pr 5381

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-fun 6504  df-fn 6505  df-f 6506  df-fo 6508

This theorem is referenced by:  f1opw2  7625  mptcnfimad  7942  imacosupp  8163  fopwdom  9027  f1opwfi  9270  enfin2i  10245  fin1a2lem7  10330  fsumss  15662  fprodss  15885  gicsubgen  19225  coe1mul2lem2  22227  cncmp  23353  cnconn  23383  qtoprest  23678  qtopomap  23679  qtopcmap  23680  hmeoimaf1o  23731  elfm3  23911  imasf1oxms  24450  mbfimaopnlem  25629  cvmsss2  35496  diaintclN  41463  dibintclN  41572  dihintcl  41749  lnmepi  43471  pwfi2f1o  43482  sge0f1o  46769  isubgr3stgrlem8  48362