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

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

Proof of Theorem foimacnv
StepHypRef Expression
1 resima 6015 . 2 ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = (𝐹 “ (𝐹𝐶))
2 fofun 6806 . . . . . 6 (𝐹:𝐴onto𝐵 → Fun 𝐹)
32adantr 481 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun 𝐹)
4 funcnvres2 6628 . . . . 5 (Fun 𝐹(𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
53, 4syl 17 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
65imaeq1d 6058 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)))
7 resss 6006 . . . . . . . . . 10 (𝐹𝐶) ⊆ 𝐹
8 cnvss 5872 . . . . . . . . . 10 ((𝐹𝐶) ⊆ 𝐹(𝐹𝐶) ⊆ 𝐹)
97, 8ax-mp 5 . . . . . . . . 9 (𝐹𝐶) ⊆ 𝐹
10 cnvcnvss 6193 . . . . . . . . 9 𝐹𝐹
119, 10sstri 3991 . . . . . . . 8 (𝐹𝐶) ⊆ 𝐹
12 funss 6567 . . . . . . . 8 ((𝐹𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐶)))
1311, 2, 12mpsyl 68 . . . . . . 7 (𝐹:𝐴onto𝐵 → Fun (𝐹𝐶))
1413adantr 481 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun (𝐹𝐶))
15 df-ima 5689 . . . . . . 7 (𝐹𝐶) = ran (𝐹𝐶)
16 df-rn 5687 . . . . . . 7 ran (𝐹𝐶) = dom (𝐹𝐶)
1715, 16eqtr2i 2761 . . . . . 6 dom (𝐹𝐶) = (𝐹𝐶)
18 df-fn 6546 . . . . . 6 ((𝐹𝐶) Fn (𝐹𝐶) ↔ (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
1914, 17, 18sylanblrc 590 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) Fn (𝐹𝐶))
20 dfdm4 5895 . . . . . 6 dom (𝐹𝐶) = ran (𝐹𝐶)
21 forn 6808 . . . . . . . . . 10 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
2221sseq2d 4014 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → (𝐶 ⊆ ran 𝐹𝐶𝐵))
2322biimpar 478 . . . . . . . 8 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ ran 𝐹)
24 df-rn 5687 . . . . . . . 8 ran 𝐹 = dom 𝐹
2523, 24sseqtrdi 4032 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ dom 𝐹)
26 ssdmres 6004 . . . . . . 7 (𝐶 ⊆ dom 𝐹 ↔ dom (𝐹𝐶) = 𝐶)
2725, 26sylib 217 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → dom (𝐹𝐶) = 𝐶)
2820, 27eqtr3id 2786 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → ran (𝐹𝐶) = 𝐶)
29 df-fo 6549 . . . . 5 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 ↔ ((𝐹𝐶) Fn (𝐹𝐶) ∧ ran (𝐹𝐶) = 𝐶))
3019, 28, 29sylanbrc 583 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶):(𝐹𝐶)–onto𝐶)
31 foima 6810 . . . 4 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
3230, 31syl 17 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
336, 32eqtr3d 2774 . 2 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = 𝐶)
341, 33eqtr3id 2786 1 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹 “ (𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wss 3948  ccnv 5675  dom cdm 5676  ran crn 5677  cres 5678  cima 5679  Fun wfun 6537   Fn wfn 6538  ontowfo 6541
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-fun 6545  df-fn 6546  df-f 6547  df-fo 6549
This theorem is referenced by:  f1opw2  7663  imacosupp  8196  fopwdom  9082  f1opwfi  9358  enfin2i  10318  fin1a2lem7  10403  fsumss  15675  fprodss  15896  gicsubgen  19193  coe1mul2lem2  22010  cncmp  23116  cnconn  23146  qtoprest  23441  qtopomap  23442  qtopcmap  23443  hmeoimaf1o  23494  elfm3  23674  imasf1oxms  24218  mbfimaopnlem  25396  cvmsss2  34551  diaintclN  40232  dibintclN  40341  dihintcl  40518  lnmepi  42129  pwfi2f1o  42140  sge0f1o  45397
  Copyright terms: Public domain W3C validator