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

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

Proof of Theorem foimacnv
StepHypRef Expression
1 resima 5581 . 2 ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = (𝐹 “ (𝐹𝐶))
2 fofun 6269 . . . . . 6 (𝐹:𝐴onto𝐵 → Fun 𝐹)
32adantr 472 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun 𝐹)
4 funcnvres2 6122 . . . . 5 (Fun 𝐹(𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
53, 4syl 17 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
65imaeq1d 5615 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)))
7 resss 5572 . . . . . . . . . . 11 (𝐹𝐶) ⊆ 𝐹
8 cnvss 5442 . . . . . . . . . . 11 ((𝐹𝐶) ⊆ 𝐹(𝐹𝐶) ⊆ 𝐹)
97, 8ax-mp 5 . . . . . . . . . 10 (𝐹𝐶) ⊆ 𝐹
10 cnvcnvss 5739 . . . . . . . . . 10 𝐹𝐹
119, 10sstri 3745 . . . . . . . . 9 (𝐹𝐶) ⊆ 𝐹
12 funss 6060 . . . . . . . . 9 ((𝐹𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐶)))
1311, 2, 12mpsyl 68 . . . . . . . 8 (𝐹:𝐴onto𝐵 → Fun (𝐹𝐶))
1413adantr 472 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun (𝐹𝐶))
15 df-ima 5271 . . . . . . . 8 (𝐹𝐶) = ran (𝐹𝐶)
16 df-rn 5269 . . . . . . . 8 ran (𝐹𝐶) = dom (𝐹𝐶)
1715, 16eqtr2i 2775 . . . . . . 7 dom (𝐹𝐶) = (𝐹𝐶)
1814, 17jctir 562 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
19 df-fn 6044 . . . . . 6 ((𝐹𝐶) Fn (𝐹𝐶) ↔ (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
2018, 19sylibr 224 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) Fn (𝐹𝐶))
21 dfdm4 5463 . . . . . 6 dom (𝐹𝐶) = ran (𝐹𝐶)
22 forn 6271 . . . . . . . . . 10 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
2322sseq2d 3766 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → (𝐶 ⊆ ran 𝐹𝐶𝐵))
2423biimpar 503 . . . . . . . 8 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ ran 𝐹)
25 df-rn 5269 . . . . . . . 8 ran 𝐹 = dom 𝐹
2624, 25syl6sseq 3784 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ dom 𝐹)
27 ssdmres 5570 . . . . . . 7 (𝐶 ⊆ dom 𝐹 ↔ dom (𝐹𝐶) = 𝐶)
2826, 27sylib 208 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → dom (𝐹𝐶) = 𝐶)
2921, 28syl5eqr 2800 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → ran (𝐹𝐶) = 𝐶)
30 df-fo 6047 . . . . 5 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 ↔ ((𝐹𝐶) Fn (𝐹𝐶) ∧ ran (𝐹𝐶) = 𝐶))
3120, 29, 30sylanbrc 701 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶):(𝐹𝐶)–onto𝐶)
32 foima 6273 . . . 4 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
3331, 32syl 17 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
346, 33eqtr3d 2788 . 2 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = 𝐶)
351, 34syl5eqr 2800 1 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹 “ (𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1624  wss 3707  ccnv 5257  dom cdm 5258  ran crn 5259  cres 5260  cima 5261  Fun wfun 6035   Fn wfn 6036  ontowfo 6039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-sep 4925  ax-nul 4933  ax-pr 5047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ral 3047  df-rex 3048  df-rab 3051  df-v 3334  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-nul 4051  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-br 4797  df-opab 4857  df-id 5166  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-fun 6043  df-fn 6044  df-f 6045  df-fo 6047
This theorem is referenced by:  f1opw2  7045  imacosupp  7496  fopwdom  8225  f1opwfi  8427  enfin2i  9327  fin1a2lem7  9412  fsumss  14647  fprodss  14869  gicsubgen  17913  coe1mul2lem2  19832  cncmp  21389  cnconn  21419  qtoprest  21714  qtopomap  21715  qtopcmap  21716  hmeoimaf1o  21767  elfm3  21947  imasf1oxms  22487  mbfimaopnlem  23613  cvmsss2  31555  diaintclN  36841  dibintclN  36950  dihintcl  37127  lnmepi  38149  pwfi2f1o  38160  sge0f1o  41094
  Copyright terms: Public domain W3C validator