Theorem f1ocnvfv2 7218

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 6795	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6828	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6780	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6768	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6926	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7113	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2772	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   I cid 5517  ^◡ccnv 5622   ↾ cres 5625   ∘ ccom 5627  ⟶wf 6482  –1-1-onto→wf1o 6485  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494

This theorem is referenced by:  f1ocnvfvb  7220  fveqf1o  7243  isocnv  7271  f1oiso2  7293  weniso  7295  dif1enlem  9080  dif1enlemOLD  9081  dif1en  9084  dif1enOLD  9086  ordiso2  9426  cantnfle  9586  cantnfp1lem3  9595  cantnflem1b  9601  cantnflem1d  9603  cantnflem1  9604  cnfcom2lem  9616  cnfcom2  9617  cnfcom3lem  9618  acndom2  9967  iunfictbso  10027  ttukeylem7  10428  fpwwe2lem5  10548  fpwwe2lem6  10549  uzrdglem  13883  uzrdgsuci  13886  fzennn  13894  axdc4uzlem  13909  seqf1olem1  13967  seqf1olem2  13968  hashfz1  14272  seqcoll  14390  seqcoll2  14391  summolem3  15640  summolem2a  15641  ackbijnn  15754  prodmolem3  15859  prodmolem2a  15860  sadcaddlem  16387  sadaddlem  16396  sadasslem  16400  sadeq  16402  phimullem  16709  eulerthlem2  16712  catcisolem  18036  mgmhmf1o  18593  mhmf1o  18689  ghmf1o  19146  f1omvdconj  19344  gsumval3eu  19802  gsumval3  19805  rngisom1  20370  fidomndrnglem  20676  lmhmf1o  20969  basqtop  23615  tgqtop  23616  ordthmeolem  23705  symgtgp  24010  imasf1obl  24393  xrhmeo  24861  ovoliunlem2  25421  vitalilem2  25527  dvcnvlem  25897  dvcnv  25898  dvcnvre  25941  efif1olem4  26471  eff1olem  26474  eflog  26502  dvrelog  26563  dvlog  26577  asinrebnd  26828  sqff1o  27109  lgsqrlem4  27277  noseqrdglem  28223  noseqrdgsuc  28226  cnvmot  28505  f1otrg  28835  f1otrge  28836  axcontlem10  28937  usgrnbcnvfv  29329  wlkiswwlks2lem4  29836  clwlkclwwlklem2a4  29960  cnvunop  31881  unopadj  31882  bracnvbra  32076  ccatws1f1o  32912  mndlactf1o  33003  mndractf1o  33004  abliso  33009  cycpmco2lem4  33090  cycpmco2lem5  33091  cycpmco2lem6  33092  cycpmco2lem7  33093  cycpmco2  33094  mndpluscn  33912  cvmfolem  35271  cvmliftlem6  35282  f1ocan1fv  37725  ismtycnv  37801  ismtyima  37802  ismtybndlem  37805  rngoisocnv  37980  lautcnvle  40088  lautcvr  40091  lautj  40092  lautm  40093  ltrncnvatb  40137  ltrncnvel  40141  ltrncnv  40145  ltrneq2  40147  cdlemg17h  40667  diainN  41056  diasslssN  41058  doca3N  41126  dihcnvid2  41272  dochocss  41365  mapdcnvid2  41656  sticksstones19  42158  rmxyval  42908  brpermmodelcnv  44998  permaxrep  45000  isuspgrim0lem  47897  isuspgrim0  47898  upgrimwlklem3  47903  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  uspgrlimlem1  47992  uspgrlimlem2  47993  uspgrlimlem3  47994  uspgrlimlem4  47995  grlicsym  48017  imaf1homlem  49112  uptrar  49221