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

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

Proof of Theorem foimacnv
StepHypRef Expression
1 resima 6020 . 2 ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = (𝐹 “ (𝐹𝐶))
2 fofun 6811 . . . . . 6 (𝐹:𝐴onto𝐵 → Fun 𝐹)
32adantr 479 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun 𝐹)
4 funcnvres2 6634 . . . . 5 (Fun 𝐹(𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
53, 4syl 17 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) = (𝐹 ↾ (𝐹𝐶)))
65imaeq1d 6063 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)))
7 resss 6007 . . . . . . . . . 10 (𝐹𝐶) ⊆ 𝐹
8 cnvss 5875 . . . . . . . . . 10 ((𝐹𝐶) ⊆ 𝐹(𝐹𝐶) ⊆ 𝐹)
97, 8ax-mp 5 . . . . . . . . 9 (𝐹𝐶) ⊆ 𝐹
10 cnvcnvss 6200 . . . . . . . . 9 𝐹𝐹
119, 10sstri 3986 . . . . . . . 8 (𝐹𝐶) ⊆ 𝐹
12 funss 6573 . . . . . . . 8 ((𝐹𝐶) ⊆ 𝐹 → (Fun 𝐹 → Fun (𝐹𝐶)))
1311, 2, 12mpsyl 68 . . . . . . 7 (𝐹:𝐴onto𝐵 → Fun (𝐹𝐶))
1413adantr 479 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → Fun (𝐹𝐶))
15 df-ima 5691 . . . . . . 7 (𝐹𝐶) = ran (𝐹𝐶)
16 df-rn 5689 . . . . . . 7 ran (𝐹𝐶) = dom (𝐹𝐶)
1715, 16eqtr2i 2754 . . . . . 6 dom (𝐹𝐶) = (𝐹𝐶)
18 df-fn 6552 . . . . . 6 ((𝐹𝐶) Fn (𝐹𝐶) ↔ (Fun (𝐹𝐶) ∧ dom (𝐹𝐶) = (𝐹𝐶)))
1914, 17, 18sylanblrc 588 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶) Fn (𝐹𝐶))
20 dfdm4 5898 . . . . . 6 dom (𝐹𝐶) = ran (𝐹𝐶)
21 forn 6813 . . . . . . . . . 10 (𝐹:𝐴onto𝐵 → ran 𝐹 = 𝐵)
2221sseq2d 4009 . . . . . . . . 9 (𝐹:𝐴onto𝐵 → (𝐶 ⊆ ran 𝐹𝐶𝐵))
2322biimpar 476 . . . . . . . 8 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ ran 𝐹)
24 df-rn 5689 . . . . . . . 8 ran 𝐹 = dom 𝐹
2523, 24sseqtrdi 4027 . . . . . . 7 ((𝐹:𝐴onto𝐵𝐶𝐵) → 𝐶 ⊆ dom 𝐹)
26 ssdmres 6018 . . . . . . 7 (𝐶 ⊆ dom 𝐹 ↔ dom (𝐹𝐶) = 𝐶)
2725, 26sylib 217 . . . . . 6 ((𝐹:𝐴onto𝐵𝐶𝐵) → dom (𝐹𝐶) = 𝐶)
2820, 27eqtr3id 2779 . . . . 5 ((𝐹:𝐴onto𝐵𝐶𝐵) → ran (𝐹𝐶) = 𝐶)
29 df-fo 6555 . . . . 5 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 ↔ ((𝐹𝐶) Fn (𝐹𝐶) ∧ ran (𝐹𝐶) = 𝐶))
3019, 28, 29sylanbrc 581 . . . 4 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹𝐶):(𝐹𝐶)–onto𝐶)
31 foima 6815 . . . 4 ((𝐹𝐶):(𝐹𝐶)–onto𝐶 → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
3230, 31syl 17 . . 3 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹𝐶) “ (𝐹𝐶)) = 𝐶)
336, 32eqtr3d 2767 . 2 ((𝐹:𝐴onto𝐵𝐶𝐵) → ((𝐹 ↾ (𝐹𝐶)) “ (𝐹𝐶)) = 𝐶)
341, 33eqtr3id 2779 1 ((𝐹:𝐴onto𝐵𝐶𝐵) → (𝐹 “ (𝐹𝐶)) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wss 3944  ccnv 5677  dom cdm 5678  ran crn 5679  cres 5680  cima 5681  Fun wfun 6543   Fn wfn 6544  ontowfo 6547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6551  df-fn 6552  df-f 6553  df-fo 6555
This theorem is referenced by:  f1opw2  7676  mptcnfimad  7991  imacosupp  8215  fopwdom  9105  f1opwfi  9382  enfin2i  10346  fin1a2lem7  10431  fsumss  15707  fprodss  15928  gicsubgen  19242  coe1mul2lem2  22212  cncmp  23340  cnconn  23370  qtoprest  23665  qtopomap  23666  qtopcmap  23667  hmeoimaf1o  23718  elfm3  23898  imasf1oxms  24442  mbfimaopnlem  25628  cvmsss2  35015  diaintclN  40661  dibintclN  40770  dihintcl  40947  lnmepi  42651  pwfi2f1o  42662  sge0f1o  45908
  Copyright terms: Public domain W3C validator