Theorem f1ocnvfv2 7233

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 6809	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6844	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6794	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6782	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6941	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7129	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2780	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   I cid 5526  ^◡ccnv 5631   ↾ cres 5634   ∘ ccom 5636  ⟶wf 6496  –1-1-onto→wf1o 6499  ‘cfv 6500

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508

This theorem is referenced by:  f1ocnvfvb  7235  fveqf1o  7258  isocnv  7286  f1oiso2  7308  weniso  7310  dif1enlem  9096  dif1en  9098  ordiso2  9432  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  acndom2  9976  iunfictbso  10036  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  uzrdglem  13892  uzrdgsuci  13895  fzennn  13903  axdc4uzlem  13918  seqf1olem1  13976  seqf1olem2  13977  hashfz1  14281  seqcoll  14399  seqcoll2  14400  summolem3  15649  summolem2a  15650  ackbijnn  15763  prodmolem3  15868  prodmolem2a  15869  sadcaddlem  16396  sadaddlem  16405  sadasslem  16409  sadeq  16411  phimullem  16718  eulerthlem2  16721  catcisolem  18046  mgmhmf1o  18637  mhmf1o  18733  ghmf1o  19189  f1omvdconj  19387  gsumval3eu  19845  gsumval3  19848  rngisom1  20414  fidomndrnglem  20717  lmhmf1o  21010  basqtop  23667  tgqtop  23668  ordthmeolem  23757  symgtgp  24062  imasf1obl  24444  xrhmeo  24912  ovoliunlem2  25472  vitalilem2  25578  dvcnvlem  25948  dvcnv  25949  dvcnvre  25992  efif1olem4  26522  eff1olem  26525  eflog  26553  dvrelog  26614  dvlog  26628  asinrebnd  26879  sqff1o  27160  lgsqrlem4  27328  addonbday  28287  noseqrdglem  28313  noseqrdgsuc  28316  bdayfinlem  28494  cnvmot  28625  f1otrg  28955  f1otrge  28956  axcontlem10  29058  usgrnbcnvfv  29450  wlkiswwlks2lem4  29957  clwlkclwwlklem2a4  30084  cnvunop  32006  unopadj  32007  bracnvbra  32201  ccatws1f1o  33044  mndlactf1o  33123  mndractf1o  33124  abliso  33129  cycpmco2lem4  33223  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmco2  33227  mndpluscn  34104  cvmfolem  35495  cvmliftlem6  35506  f1ocan1fv  37977  ismtycnv  38053  ismtyima  38054  ismtybndlem  38057  rngoisocnv  38232  lautcnvle  40465  lautcvr  40468  lautj  40469  lautm  40470  ltrncnvatb  40514  ltrncnvel  40518  ltrncnv  40522  ltrneq2  40524  cdlemg17h  41044  diainN  41433  diasslssN  41435  doca3N  41503  dihcnvid2  41649  dochocss  41742  mapdcnvid2  42033  sticksstones19  42535  rmxyval  43272  brpermmodelcnv  45360  permaxrep  45362  isuspgrim0lem  48253  isuspgrim0  48254  upgrimwlklem3  48259  uhgrimisgrgriclem  48290  clnbgrgrimlem  48293  uspgrlimlem1  48348  uspgrlimlem2  48349  uspgrlimlem3  48350  uspgrlimlem4  48351  grlicsym  48373  imaf1homlem  49466  uptrar  49575