Theorem f1ocnvfv2 7270

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   I cid 5547  ^◡ccnv 5653   ↾ cres 5656   ∘ ccom 5658  ⟶wf 6527  –1-1-onto→wf1o 6530  ‘cfv 6531

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539

This theorem is referenced by:  f1ocnvfvb  7272  fveqf1o  7295  isocnv  7323  f1oiso2  7345  weniso  7347  dif1enlem  9170  dif1enlemOLD  9171  dif1en  9174  dif1enOLD  9176  ordiso2  9529  cantnfle  9685  cantnfp1lem3  9694  cantnflem1b  9700  cantnflem1d  9702  cantnflem1  9703  cnfcom2lem  9715  cnfcom2  9716  cnfcom3lem  9717  acndom2  10068  iunfictbso  10128  ttukeylem7  10529  fpwwe2lem5  10649  fpwwe2lem6  10650  uzrdglem  13975  uzrdgsuci  13978  fzennn  13986  axdc4uzlem  14001  seqf1olem1  14059  seqf1olem2  14060  hashfz1  14364  seqcoll  14482  seqcoll2  14483  summolem3  15730  summolem2a  15731  ackbijnn  15844  prodmolem3  15949  prodmolem2a  15950  sadcaddlem  16476  sadaddlem  16485  sadasslem  16489  sadeq  16491  phimullem  16798  eulerthlem2  16801  catcisolem  18123  mgmhmf1o  18678  mhmf1o  18774  ghmf1o  19231  f1omvdconj  19427  gsumval3eu  19885  gsumval3  19888  rngisom1  20426  fidomndrnglem  20732  lmhmf1o  21004  basqtop  23649  tgqtop  23650  ordthmeolem  23739  symgtgp  24044  imasf1obl  24427  xrhmeo  24895  ovoliunlem2  25456  vitalilem2  25562  dvcnvlem  25932  dvcnv  25933  dvcnvre  25976  efif1olem4  26506  eff1olem  26509  eflog  26537  dvrelog  26598  dvlog  26612  asinrebnd  26863  sqff1o  27144  lgsqrlem4  27312  noseqrdglem  28251  noseqrdgsuc  28254  cnvmot  28520  f1otrg  28850  f1otrge  28851  axcontlem10  28952  usgrnbcnvfv  29344  wlkiswwlks2lem4  29854  clwlkclwwlklem2a4  29978  cnvunop  31899  unopadj  31900  bracnvbra  32094  ccatws1f1o  32927  mndlactf1o  33025  mndractf1o  33026  abliso  33031  cycpmco2lem4  33140  cycpmco2lem5  33141  cycpmco2lem6  33142  cycpmco2lem7  33143  cycpmco2  33144  mndpluscn  33957  cvmfolem  35301  cvmliftlem6  35312  f1ocan1fv  37750  ismtycnv  37826  ismtyima  37827  ismtybndlem  37830  rngoisocnv  38005  lautcnvle  40108  lautcvr  40111  lautj  40112  lautm  40113  ltrncnvatb  40157  ltrncnvel  40161  ltrncnv  40165  ltrneq2  40167  cdlemg17h  40687  diainN  41076  diasslssN  41078  doca3N  41146  dihcnvid2  41292  dochocss  41385  mapdcnvid2  41676  sticksstones19  42178  rmxyval  42939  brpermmodelcnv  45029  permaxrep  45031  isuspgrim0lem  47906  isuspgrim0  47907  upgrimwlklem3  47912  uhgrimisgrgriclem  47943  clnbgrgrimlem  47946  uspgrlimlem1  48000  uspgrlimlem2  48001  uspgrlimlem3  48002  uspgrlimlem4  48003  grlicsym  48018  imaf1homlem  49066