MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  foimacnv Structured version   Visualization version   GIF version

Theorem foimacnv 6395
Description: A reverse version of f1imacnv 6394. (Contributed by Jeff Hankins, 16-Jul-2009.)
Assertion
Ref Expression
foimacnv ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹 “ (𝐹𝐶)) = 𝐶)

Proof of Theorem foimacnv
StepHypRef Expression
1 resima 5667 . 2 ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = (𝐹 “ (𝐹𝐶))
2 fofun 6354 . . . . . 6 (𝐹:𝐴onto𝐵 → Fun 𝐹)
32adantr 474 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun 𝐹)
4 funcnvres2 6202 . . . . 5 (Fun 𝐹(𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
53, 4syl 17 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
65imaeq1d 5706 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)))
7 resss 5658 . . . . . . . . . . 11 (𝐹𝐶) ⊆ 𝐹
8 cnvss 5527 . . . . . . . . . . 11 ((𝐹𝐶) ⊆ 𝐹(𝐹𝐶) ⊆ 𝐹)
97, 8ax-mp 5 . . . . . . . . . 10 (𝐹𝐶) ⊆ 𝐹
10 cnvcnvss 5829 . . . . . . . . . 10 𝐹𝐹
119, 10sstri 3836 . . . . . . . . 9 (𝐹𝐶) ⊆ 𝐹
12 funss 6142 . . . . . . . . 9 ((𝐹𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐶)))
1311, 2, 12mpsyl 68 . . . . . . . 8 (𝐹:𝐴onto𝐵 → Fun (𝐹𝐶))
1413adantr 474 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun (𝐹𝐶))
15 df-ima 5355 . . . . . . . 8 (𝐹𝐶) = ran (𝐹𝐶)
16 df-rn 5353 . . . . . . . 8 ran (𝐹𝐶) = dom (𝐹𝐶)
1715, 16eqtr2i 2850 . . . . . . 7 dom (𝐹𝐶) = (𝐹𝐶)
1814, 17jctir 518 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
19 df-fn 6126 . . . . . 6 ((𝐹𝐶) Fn (𝐹𝐶) ↔ (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
2018, 19sylibr 226 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) Fn (𝐹𝐶))
21 dfdm4 5548 . . . . . 6 dom (𝐹𝐶) = ran (𝐹𝐶)
22 forn 6356 . . . . . . . . . 10 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
2322sseq2d 3858 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → (𝐶 ⊆ ran 𝐹𝐶𝐵))
2423biimpar 471 . . . . . . . 8 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ ran 𝐹)
25 df-rn 5353 . . . . . . . 8 ran 𝐹 = dom 𝐹
2624, 25syl6sseq 3876 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ dom 𝐹)
27 ssdmres 5656 . . . . . . 7 (𝐶 ⊆ dom 𝐹 ↔ dom (𝐹𝐶) = 𝐶)
2826, 27sylib 210 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → dom (𝐹𝐶) = 𝐶)
2921, 28syl5eqr 2875 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → ran (𝐹𝐶) = 𝐶)
30 df-fo 6129 . . . . 5 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 ↔ ((𝐹𝐶) Fn (𝐹𝐶) ∧ ran (𝐹𝐶) = 𝐶))
3120, 29, 30sylanbrc 580 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶):(𝐹𝐶)–onto𝐶)
32 foima 6358 . . . 4 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
3331, 32syl 17 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
346, 33eqtr3d 2863 . 2 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = 𝐶)
351, 34syl5eqr 2875 1 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹 “ (𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1658  wss 3798  ccnv 5341  dom cdm 5342  ran crn 5343  cres 5344  cima 5345  Fun wfun 6117   Fn wfn 6118  ontowfo 6121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-fun 6125  df-fn 6126  df-f 6127  df-fo 6129
This theorem is referenced by:  f1opw2  7148  imacosupp  7600  fopwdom  8337  f1opwfi  8539  enfin2i  9458  fin1a2lem7  9543  fsumss  14833  fprodss  15051  gicsubgen  18071  coe1mul2lem2  19998  cncmp  21566  cnconn  21596  qtoprest  21891  qtopomap  21892  qtopcmap  21893  hmeoimaf1o  21944  elfm3  22124  imasf1oxms  22664  mbfimaopnlem  23821  cvmsss2  31802  diaintclN  37133  dibintclN  37242  dihintcl  37419  lnmepi  38498  pwfi2f1o  38509  sge0f1o  41390
  Copyright terms: Public domain W3C validator