Theorem f1ocnvfv2 7225

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 6801	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6836	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6786	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6774	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6933	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7121	. . 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 5518  ^◡ccnv 5623   ↾ cres 5626   ∘ ccom 5628  ⟶wf 6488  –1-1-onto→wf1o 6491  ‘cfv 6492

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 5231  ax-nul 5241  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500

This theorem is referenced by:  f1ocnvfvb  7227  fveqf1o  7250  isocnv  7278  f1oiso2  7300  weniso  7302  dif1enlem  9087  dif1en  9089  ordiso2  9423  cantnfle  9583  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  cnfcom2lem  9613  cnfcom2  9614  cnfcom3lem  9615  acndom2  9967  iunfictbso  10027  ttukeylem7  10428  fpwwe2lem5  10549  fpwwe2lem6  10550  uzrdglem  13910  uzrdgsuci  13913  fzennn  13921  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  hashfz1  14299  seqcoll  14417  seqcoll2  14418  summolem3  15667  summolem2a  15668  ackbijnn  15784  prodmolem3  15889  prodmolem2a  15890  sadcaddlem  16417  sadaddlem  16426  sadasslem  16430  sadeq  16432  phimullem  16740  eulerthlem2  16743  catcisolem  18068  mgmhmf1o  18659  mhmf1o  18755  ghmf1o  19214  f1omvdconj  19412  gsumval3eu  19870  gsumval3  19873  rngisom1  20437  fidomndrnglem  20740  lmhmf1o  21033  basqtop  23686  tgqtop  23687  ordthmeolem  23776  symgtgp  24081  imasf1obl  24463  xrhmeo  24923  ovoliunlem2  25480  vitalilem2  25586  dvcnvlem  25953  dvcnv  25954  dvcnvre  25996  efif1olem4  26522  eff1olem  26525  eflog  26553  dvrelog  26614  dvlog  26628  asinrebnd  26878  sqff1o  27159  lgsqrlem4  27326  addonbday  28285  noseqrdglem  28311  noseqrdgsuc  28314  bdayfinlem  28492  cnvmot  28623  f1otrg  28953  f1otrge  28954  axcontlem10  29056  usgrnbcnvfv  29448  wlkiswwlks2lem4  29955  clwlkclwwlklem2a4  30082  cnvunop  32004  unopadj  32005  bracnvbra  32199  ccatws1f1o  33026  mndlactf1o  33105  mndractf1o  33106  abliso  33111  cycpmco2lem4  33205  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmco2  33209  mndpluscn  34086  cvmfolem  35477  cvmliftlem6  35488  f1ocan1fv  38061  ismtycnv  38137  ismtyima  38138  ismtybndlem  38141  rngoisocnv  38316  lautcnvle  40549  lautcvr  40552  lautj  40553  lautm  40554  ltrncnvatb  40598  ltrncnvel  40602  ltrncnv  40606  ltrneq2  40608  cdlemg17h  41128  diainN  41517  diasslssN  41519  doca3N  41587  dihcnvid2  41733  dochocss  41826  mapdcnvid2  42117  sticksstones19  42618  rmxyval  43361  brpermmodelcnv  45449  permaxrep  45451  isuspgrim0lem  48381  isuspgrim0  48382  upgrimwlklem3  48387  uhgrimisgrgriclem  48418  clnbgrgrimlem  48421  uspgrlimlem1  48476  uspgrlimlem2  48477  uspgrlimlem3  48478  uspgrlimlem4  48479  grlicsym  48501  imaf1homlem  49594  uptrar  49703