Theorem f1ocnvfv2 7232

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 6807	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6842	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6792	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6780	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6939	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7128	. . 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 1542   ∈ wcel 2114   I cid 5525  ^◡ccnv 5630   ↾ cres 5633   ∘ ccom 5635  ⟶wf 6494  –1-1-onto→wf1o 6497  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506

This theorem is referenced by:  f1ocnvfvb  7234  fveqf1o  7257  isocnv  7285  f1oiso2  7307  weniso  7309  dif1enlem  9094  dif1en  9096  ordiso2  9430  cantnfle  9592  cantnfp1lem3  9601  cantnflem1b  9607  cantnflem1d  9609  cantnflem1  9610  cnfcom2lem  9622  cnfcom2  9623  cnfcom3lem  9624  acndom2  9976  iunfictbso  10036  ttukeylem7  10437  fpwwe2lem5  10558  fpwwe2lem6  10559  uzrdglem  13919  uzrdgsuci  13922  fzennn  13930  axdc4uzlem  13945  seqf1olem1  14003  seqf1olem2  14004  hashfz1  14308  seqcoll  14426  seqcoll2  14427  summolem3  15676  summolem2a  15677  ackbijnn  15793  prodmolem3  15898  prodmolem2a  15899  sadcaddlem  16426  sadaddlem  16435  sadasslem  16439  sadeq  16441  phimullem  16749  eulerthlem2  16752  catcisolem  18077  mgmhmf1o  18668  mhmf1o  18764  ghmf1o  19223  f1omvdconj  19421  gsumval3eu  19879  gsumval3  19882  rngisom1  20446  fidomndrnglem  20749  lmhmf1o  21041  basqtop  23676  tgqtop  23677  ordthmeolem  23766  symgtgp  24071  imasf1obl  24453  xrhmeo  24913  ovoliunlem2  25470  vitalilem2  25576  dvcnvlem  25943  dvcnv  25944  dvcnvre  25986  efif1olem4  26509  eff1olem  26512  eflog  26540  dvrelog  26601  dvlog  26615  asinrebnd  26865  sqff1o  27145  lgsqrlem4  27312  addonbday  28271  noseqrdglem  28297  noseqrdgsuc  28300  bdayfinlem  28478  cnvmot  28609  f1otrg  28939  f1otrge  28940  axcontlem10  29042  usgrnbcnvfv  29434  wlkiswwlks2lem4  29940  clwlkclwwlklem2a4  30067  cnvunop  31989  unopadj  31990  bracnvbra  32184  ccatws1f1o  33011  mndlactf1o  33090  mndractf1o  33091  abliso  33096  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmco2  33194  mndpluscn  34070  cvmfolem  35461  cvmliftlem6  35472  f1ocan1fv  38047  ismtycnv  38123  ismtyima  38124  ismtybndlem  38127  rngoisocnv  38302  lautcnvle  40535  lautcvr  40538  lautj  40539  lautm  40540  ltrncnvatb  40584  ltrncnvel  40588  ltrncnv  40592  ltrneq2  40594  cdlemg17h  41114  diainN  41503  diasslssN  41505  doca3N  41573  dihcnvid2  41719  dochocss  41812  mapdcnvid2  42103  sticksstones19  42604  rmxyval  43343  brpermmodelcnv  45431  permaxrep  45433  isuspgrim0lem  48369  isuspgrim0  48370  upgrimwlklem3  48375  uhgrimisgrgriclem  48406  clnbgrgrimlem  48409  uspgrlimlem1  48464  uspgrlimlem2  48465  uspgrlimlem3  48466  uspgrlimlem4  48467  grlicsym  48489  imaf1homlem  49582  uptrar  49691