Theorem f1ocnvfv2 7283

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 6850	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6885	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6835	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6822	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6983	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7176	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2804	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   I cid 5545  ^◡ccnv 5650   ↾ cres 5653   ∘ ccom 5655  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  f1ocnvfvb  7285  fveqf1o  7308  isocnv  7336  f1oiso2  7358  weniso  7362  dif1enlem  9168  dif1en  9170  ordiso2  9502  cantnfle  9665  cantnfp1lem3  9674  cantnflem1b  9680  cantnflem1d  9682  cantnflem1  9683  cnfcom2lem  9695  cnfcom2  9696  cnfcom3lem  9697  acndom2  10126  iunfictbso  10186  ttukeylem7  10586  fpwwe2lem5  10713  fpwwe2lem6  10714  uzrdglem  14093  uzrdgsuci  14096  fzennn  14104  axdc4uzlem  14119  seqf1olem1  14177  seqf1olem2  14178  hashfz1  14483  seqcoll  14602  seqcoll2  14603  summolem3  15873  summolem2a  15874  ackbijnn  15990  prodmolem3  16093  prodmolem2a  16094  sadcaddlem  16620  sadaddlem  16629  sadasslem  16633  sadeq  16635  phimullem  16949  eulerthlem2  16952  catcisolem  18278  mgmhmf1o  18882  mhmf1o  18984  ghmf1o  19455  f1omvdconj  19653  gsumval3eu  20111  gsumval3  20114  rngisom1  20689  fidomndrnglem  21023  lmhmf1o  21314  basqtop  24023  tgqtop  24024  ordthmeolem  24113  symgtgp  24418  imasf1obl  24800  xrhmeo  25260  ovoliunlem2  25817  vitalilem2  25923  dvcnvlem  26289  dvcnv  26290  dvcnvre  26332  efif1olem4  26866  eff1olem  26869  eflog  26897  dvrelog  26958  dvlog  26972  asinrebnd  27222  sqff1o  27502  lgsqrlem4  27669  addonbday  28658  noseqrdglem  28684  noseqrdgsuc  28687  bdayfinlem  28865  cnvmot  28997  f1otrg  29441  f1otrge  29442  axcontlem10  29544  usgrnbcnvfv  29939  wlkiswwlks2lem4  30454  clwlkclwwlklem2a4  30581  cnvunop  32513  unopadj  32514  bracnvbra  32708  ccatws1f1o  33507  mndlactf1o  33584  mndractf1o  33585  abliso  33589  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2lem7  33686  cycpmco2  33687  mndpluscn  34551  vonf1oonfo  35877  cvmfolem  36023  cvmliftlem6  36034  f1ocan1fv  38640  ismtycnv  38716  ismtyima  38717  ismtybndlem  38720  rngoisocnv  38895  lautcnvle  41126  lautcvr  41129  lautj  41130  lautm  41131  ltrncnvatb  41175  ltrncnvel  41179  ltrncnv  41183  ltrneq2  41185  cdlemg17h  41705  diainN  42094  diasslssN  42096  doca3N  42164  dihcnvid2  42310  dochocss  42403  mapdcnvid2  42694  sticksstones19  43195  rmxyval  43901  brpermmodelcnv  45972  permaxrep  45974  isuspgrim0lem  48960  isuspgrim0  48961  upgrimwlklem3  48966  uhgrimisgrgriclem  48997  clnbgrgrimlem  49000  uspgrlimlem1  49055  uspgrlimlem2  49056  uspgrlimlem3  49057  uspgrlimlem4  49058  grlicsym  49080  imaf1homlem  50184  uptrar  50293