Theorem f1ocnvfv2 7223

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 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7119	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2779	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  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  7225  fveqf1o  7248  isocnv  7276  f1oiso2  7298  weniso  7300  dif1enlem  9084  dif1en  9086  ordiso2  9420  cantnfle  9580  cantnfp1lem3  9589  cantnflem1b  9595  cantnflem1d  9597  cantnflem1  9598  cnfcom2lem  9610  cnfcom2  9611  cnfcom3lem  9612  acndom2  9964  iunfictbso  10024  ttukeylem7  10425  fpwwe2lem5  10546  fpwwe2lem6  10547  uzrdglem  13880  uzrdgsuci  13883  fzennn  13891  axdc4uzlem  13906  seqf1olem1  13964  seqf1olem2  13965  hashfz1  14269  seqcoll  14387  seqcoll2  14388  summolem3  15637  summolem2a  15638  ackbijnn  15751  prodmolem3  15856  prodmolem2a  15857  sadcaddlem  16384  sadaddlem  16393  sadasslem  16397  sadeq  16399  phimullem  16706  eulerthlem2  16709  catcisolem  18034  mgmhmf1o  18625  mhmf1o  18721  ghmf1o  19177  f1omvdconj  19375  gsumval3eu  19833  gsumval3  19836  rngisom1  20402  fidomndrnglem  20705  lmhmf1o  20998  basqtop  23655  tgqtop  23656  ordthmeolem  23745  symgtgp  24050  imasf1obl  24432  xrhmeo  24900  ovoliunlem2  25460  vitalilem2  25566  dvcnvlem  25936  dvcnv  25937  dvcnvre  25980  efif1olem4  26510  eff1olem  26513  eflog  26541  dvrelog  26602  dvlog  26616  asinrebnd  26867  sqff1o  27148  lgsqrlem4  27316  addonbday  28275  noseqrdglem  28301  noseqrdgsuc  28304  bdayfinlem  28482  cnvmot  28613  f1otrg  28943  f1otrge  28944  axcontlem10  29046  usgrnbcnvfv  29438  wlkiswwlks2lem4  29945  clwlkclwwlklem2a4  30072  cnvunop  31993  unopadj  31994  bracnvbra  32188  ccatws1f1o  33033  mndlactf1o  33112  mndractf1o  33113  abliso  33118  cycpmco2lem4  33211  cycpmco2lem5  33212  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmco2  33215  mndpluscn  34083  cvmfolem  35473  cvmliftlem6  35484  f1ocan1fv  37927  ismtycnv  38003  ismtyima  38004  ismtybndlem  38007  rngoisocnv  38182  lautcnvle  40349  lautcvr  40352  lautj  40353  lautm  40354  ltrncnvatb  40398  ltrncnvel  40402  ltrncnv  40406  ltrneq2  40408  cdlemg17h  40928  diainN  41317  diasslssN  41319  doca3N  41387  dihcnvid2  41533  dochocss  41626  mapdcnvid2  41917  sticksstones19  42419  rmxyval  43157  brpermmodelcnv  45245  permaxrep  45247  isuspgrim0lem  48139  isuspgrim0  48140  upgrimwlklem3  48145  uhgrimisgrgriclem  48176  clnbgrgrimlem  48179  uspgrlimlem1  48234  uspgrlimlem2  48235  uspgrlimlem3  48236  uspgrlimlem4  48237  grlicsym  48259  imaf1homlem  49352  uptrar  49461