Theorem f1ocnvfv2 7234

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 6809	. . . 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 6794	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6782	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6942	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7129	. . 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 5525  ^◡ccnv 5630   ↾ cres 5633   ∘ ccom 5635  ⟶wf 6495  –1-1-onto→wf1o 6498  ‘cfv 6499

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 5246  ax-nul 5256  ax-pr 5382

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 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  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 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507

This theorem is referenced by:  f1ocnvfvb  7236  fveqf1o  7259  isocnv  7287  f1oiso2  7309  weniso  7311  dif1enlem  9097  dif1enlemOLD  9098  dif1en  9101  dif1enOLD  9103  ordiso2  9444  cantnfle  9600  cantnfp1lem3  9609  cantnflem1b  9615  cantnflem1d  9617  cantnflem1  9618  cnfcom2lem  9630  cnfcom2  9631  cnfcom3lem  9632  acndom2  9983  iunfictbso  10043  ttukeylem7  10444  fpwwe2lem5  10564  fpwwe2lem6  10565  uzrdglem  13898  uzrdgsuci  13901  fzennn  13909  axdc4uzlem  13924  seqf1olem1  13982  seqf1olem2  13983  hashfz1  14287  seqcoll  14405  seqcoll2  14406  summolem3  15656  summolem2a  15657  ackbijnn  15770  prodmolem3  15875  prodmolem2a  15876  sadcaddlem  16403  sadaddlem  16412  sadasslem  16416  sadeq  16418  phimullem  16725  eulerthlem2  16728  catcisolem  18048  mgmhmf1o  18603  mhmf1o  18699  ghmf1o  19156  f1omvdconj  19352  gsumval3eu  19810  gsumval3  19813  rngisom1  20351  fidomndrnglem  20657  lmhmf1o  20929  basqtop  23574  tgqtop  23575  ordthmeolem  23664  symgtgp  23969  imasf1obl  24352  xrhmeo  24820  ovoliunlem2  25380  vitalilem2  25486  dvcnvlem  25856  dvcnv  25857  dvcnvre  25900  efif1olem4  26430  eff1olem  26433  eflog  26461  dvrelog  26522  dvlog  26536  asinrebnd  26787  sqff1o  27068  lgsqrlem4  27236  noseqrdglem  28175  noseqrdgsuc  28178  cnvmot  28444  f1otrg  28774  f1otrge  28775  axcontlem10  28876  usgrnbcnvfv  29268  wlkiswwlks2lem4  29775  clwlkclwwlklem2a4  29899  cnvunop  31820  unopadj  31821  bracnvbra  32015  ccatws1f1o  32846  mndlactf1o  32944  mndractf1o  32945  abliso  32950  cycpmco2lem4  33059  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2lem7  33062  cycpmco2  33063  mndpluscn  33889  cvmfolem  35239  cvmliftlem6  35250  f1ocan1fv  37693  ismtycnv  37769  ismtyima  37770  ismtybndlem  37773  rngoisocnv  37948  lautcnvle  40056  lautcvr  40059  lautj  40060  lautm  40061  ltrncnvatb  40105  ltrncnvel  40109  ltrncnv  40113  ltrneq2  40115  cdlemg17h  40635  diainN  41024  diasslssN  41026  doca3N  41094  dihcnvid2  41240  dochocss  41333  mapdcnvid2  41624  sticksstones19  42126  rmxyval  42877  brpermmodelcnv  44967  permaxrep  44969  isuspgrim0lem  47866  isuspgrim0  47867  upgrimwlklem3  47872  uhgrimisgrgriclem  47903  clnbgrgrimlem  47906  uspgrlimlem1  47960  uspgrlimlem2  47961  uspgrlimlem3  47962  uspgrlimlem4  47963  grlicsym  47978  imaf1homlem  49069  uptrar  49178