Theorem f1ocnvfv2 7255

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 6830	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6863	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6815	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6803	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6963	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7150	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2773	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   I cid 5535  ^◡ccnv 5640   ↾ cres 5643   ∘ ccom 5645  ⟶wf 6510  –1-1-onto→wf1o 6513  ‘cfv 6514

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522

This theorem is referenced by:  f1ocnvfvb  7257  fveqf1o  7280  isocnv  7308  f1oiso2  7330  weniso  7332  dif1enlem  9126  dif1enlemOLD  9127  dif1en  9130  dif1enOLD  9132  ordiso2  9475  cantnfle  9631  cantnfp1lem3  9640  cantnflem1b  9646  cantnflem1d  9648  cantnflem1  9649  cnfcom2lem  9661  cnfcom2  9662  cnfcom3lem  9663  acndom2  10014  iunfictbso  10074  ttukeylem7  10475  fpwwe2lem5  10595  fpwwe2lem6  10596  uzrdglem  13929  uzrdgsuci  13932  fzennn  13940  axdc4uzlem  13955  seqf1olem1  14013  seqf1olem2  14014  hashfz1  14318  seqcoll  14436  seqcoll2  14437  summolem3  15687  summolem2a  15688  ackbijnn  15801  prodmolem3  15906  prodmolem2a  15907  sadcaddlem  16434  sadaddlem  16443  sadasslem  16447  sadeq  16449  phimullem  16756  eulerthlem2  16759  catcisolem  18079  mgmhmf1o  18634  mhmf1o  18730  ghmf1o  19187  f1omvdconj  19383  gsumval3eu  19841  gsumval3  19844  rngisom1  20382  fidomndrnglem  20688  lmhmf1o  20960  basqtop  23605  tgqtop  23606  ordthmeolem  23695  symgtgp  24000  imasf1obl  24383  xrhmeo  24851  ovoliunlem2  25411  vitalilem2  25517  dvcnvlem  25887  dvcnv  25888  dvcnvre  25931  efif1olem4  26461  eff1olem  26464  eflog  26492  dvrelog  26553  dvlog  26567  asinrebnd  26818  sqff1o  27099  lgsqrlem4  27267  noseqrdglem  28206  noseqrdgsuc  28209  cnvmot  28475  f1otrg  28805  f1otrge  28806  axcontlem10  28907  usgrnbcnvfv  29299  wlkiswwlks2lem4  29809  clwlkclwwlklem2a4  29933  cnvunop  31854  unopadj  31855  bracnvbra  32049  ccatws1f1o  32880  mndlactf1o  32978  mndractf1o  32979  abliso  32984  cycpmco2lem4  33093  cycpmco2lem5  33094  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmco2  33097  mndpluscn  33923  cvmfolem  35273  cvmliftlem6  35284  f1ocan1fv  37727  ismtycnv  37803  ismtyima  37804  ismtybndlem  37807  rngoisocnv  37982  lautcnvle  40090  lautcvr  40093  lautj  40094  lautm  40095  ltrncnvatb  40139  ltrncnvel  40143  ltrncnv  40147  ltrneq2  40149  cdlemg17h  40669  diainN  41058  diasslssN  41060  doca3N  41128  dihcnvid2  41274  dochocss  41367  mapdcnvid2  41658  sticksstones19  42160  rmxyval  42911  brpermmodelcnv  45001  permaxrep  45003  isuspgrim0lem  47897  isuspgrim0  47898  upgrimwlklem3  47903  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  uspgrlimlem1  47991  uspgrlimlem2  47992  uspgrlimlem3  47993  uspgrlimlem4  47994  grlicsym  48009  imaf1homlem  49100  uptrar  49209