Theorem f1ocnvfv2 7206

Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)

Assertion

Ref	Expression
f1ocnvfv2	⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Proof of Theorem f1ocnvfv2

Step	Hyp	Ref	Expression
1		f1ococnv2 6785	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6819	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6770	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6758	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6916	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7102	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2774	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   I cid 5505  ^◡ccnv 5610   ↾ cres 5613   ∘ ccom 5615  ⟶wf 6472  –1-1-onto→wf1o 6475  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484

This theorem is referenced by:  f1ocnvfvb  7208  fveqf1o  7231  isocnv  7259  f1oiso2  7281  weniso  7283  dif1enlem  9064  dif1en  9066  ordiso2  9396  cantnfle  9556  cantnfp1lem3  9565  cantnflem1b  9571  cantnflem1d  9573  cantnflem1  9574  cnfcom2lem  9586  cnfcom2  9587  cnfcom3lem  9588  acndom2  9940  iunfictbso  10000  ttukeylem7  10401  fpwwe2lem5  10521  fpwwe2lem6  10522  uzrdglem  13859  uzrdgsuci  13862  fzennn  13870  axdc4uzlem  13885  seqf1olem1  13943  seqf1olem2  13944  hashfz1  14248  seqcoll  14366  seqcoll2  14367  summolem3  15616  summolem2a  15617  ackbijnn  15730  prodmolem3  15835  prodmolem2a  15836  sadcaddlem  16363  sadaddlem  16372  sadasslem  16376  sadeq  16378  phimullem  16685  eulerthlem2  16688  catcisolem  18012  mgmhmf1o  18603  mhmf1o  18699  ghmf1o  19155  f1omvdconj  19353  gsumval3eu  19811  gsumval3  19814  rngisom1  20379  fidomndrnglem  20682  lmhmf1o  20975  basqtop  23621  tgqtop  23622  ordthmeolem  23711  symgtgp  24016  imasf1obl  24398  xrhmeo  24866  ovoliunlem2  25426  vitalilem2  25532  dvcnvlem  25902  dvcnv  25903  dvcnvre  25946  efif1olem4  26476  eff1olem  26479  eflog  26507  dvrelog  26568  dvlog  26582  asinrebnd  26833  sqff1o  27114  lgsqrlem4  27282  noseqrdglem  28230  noseqrdgsuc  28233  cnvmot  28514  f1otrg  28844  f1otrge  28845  axcontlem10  28946  usgrnbcnvfv  29338  wlkiswwlks2lem4  29845  clwlkclwwlklem2a4  29969  cnvunop  31890  unopadj  31891  bracnvbra  32085  ccatws1f1o  32924  mndlactf1o  33003  mndractf1o  33004  abliso  33009  cycpmco2lem4  33090  cycpmco2lem5  33091  cycpmco2lem6  33092  cycpmco2lem7  33093  cycpmco2  33094  mndpluscn  33931  cvmfolem  35315  cvmliftlem6  35326  f1ocan1fv  37766  ismtycnv  37842  ismtyima  37843  ismtybndlem  37846  rngoisocnv  38021  lautcnvle  40128  lautcvr  40131  lautj  40132  lautm  40133  ltrncnvatb  40177  ltrncnvel  40181  ltrncnv  40185  ltrneq2  40187  cdlemg17h  40707  diainN  41096  diasslssN  41098  doca3N  41166  dihcnvid2  41312  dochocss  41405  mapdcnvid2  41696  sticksstones19  42198  rmxyval  42948  brpermmodelcnv  45037  permaxrep  45039  isuspgrim0lem  47924  isuspgrim0  47925  upgrimwlklem3  47930  uhgrimisgrgriclem  47961  clnbgrgrimlem  47964  uspgrlimlem1  48019  uspgrlimlem2  48020  uspgrlimlem3  48021  uspgrlimlem4  48022  grlicsym  48044  imaf1homlem  49139  uptrar  49248