Theorem f1ocnvfv2 7281

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 6852	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6887	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6837	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6824	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6985	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7175	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2808	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   I cid 5557  ^◡ccnv 5662   ↾ cres 5665   ∘ ccom 5667  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is used by:  f1ocnvfvb  7283  fveqf1o  7306  isocnv  7334  f1oiso2  7356  weniso  7360  dif1enlem  9147  dif1en  9149  ordiso2  9480  cantnfle  9643  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1d  9660  cantnflem1  9661  cnfcom2lem  9673  cnfcom2  9674  cnfcom3lem  9675  acndom2  10050  iunfictbso  10110  ttukeylem7  10510  fpwwe2lem5  10631  fpwwe2lem6  10632  uzrdglem  14007  uzrdgsuci  14010  fzennn  14018  axdc4uzlem  14033  seqf1olem1  14091  seqf1olem2  14092  hashfz1  14396  seqcoll  14515  seqcoll2  14516  summolem3  15784  summolem2a  15785  ackbijnn  15901  prodmolem3  16006  prodmolem2a  16007  sadcaddlem  16533  sadaddlem  16542  sadasslem  16546  sadeq  16548  phimullem  16856  eulerthlem2  16859  catcisolem  18185  mgmhmf1o  18780  mhmf1o  18878  ghmf1o  19342  f1omvdconj  19540  gsumval3eu  19998  gsumval3  20001  rngisom1  20574  fidomndrnglem  20906  lmhmf1o  21197  basqtop  23899  tgqtop  23900  ordthmeolem  23989  symgtgp  24294  imasf1obl  24676  xrhmeo  25136  ovoliunlem2  25693  vitalilem2  25799  dvcnvlem  26166  dvcnv  26167  dvcnvre  26209  efif1olem4  26741  eff1olem  26744  eflog  26772  dvrelog  26833  dvlog  26847  asinrebnd  27097  sqff1o  27377  lgsqrlem4  27544  addonbday  28503  noseqrdglem  28529  noseqrdgsuc  28532  bdayfinlem  28710  cnvmot  28841  f1otrg  29251  f1otrge  29252  axcontlem10  29354  usgrnbcnvfv  29749  wlkiswwlks2lem4  30264  clwlkclwwlklem2a4  30391  cnvunop  32317  unopadj  32318  bracnvbra  32512  ccatws1f1o  33313  mndlactf1o  33390  mndractf1o  33391  abliso  33395  cycpmco2lem4  33489  cycpmco2lem5  33490  cycpmco2lem6  33491  cycpmco2lem7  33492  cycpmco2  33493  mndpluscn  34356  vonf1oonfo  35632  cvmfolem  35784  cvmliftlem6  35795  f1ocan1fv  38410  ismtycnv  38486  ismtyima  38487  ismtybndlem  38490  rngoisocnv  38665  lautcnvle  40896  lautcvr  40899  lautj  40900  lautm  40901  ltrncnvatb  40945  ltrncnvel  40949  ltrncnv  40953  ltrneq2  40955  cdlemg17h  41475  diainN  41864  diasslssN  41866  doca3N  41934  dihcnvid2  42080  dochocss  42173  mapdcnvid2  42464  sticksstones19  42965  rmxyval  43675  brpermmodelcnv  45746  permaxrep  45748  isuspgrim0lem  48691  isuspgrim0  48692  upgrimwlklem3  48697  uhgrimisgrgriclem  48728  clnbgrgrimlem  48731  uspgrlimlem1  48786  uspgrlimlem2  48787  uspgrlimlem3  48788  uspgrlimlem4  48789  grlicsym  48811  imaf1homlem  49918  uptrar  50027