Theorem f1ocnvfv2 7286

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 6853	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6888	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6838	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6825	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6986	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7179	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2803	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   I cid 5544  ^◡ccnv 5649   ↾ cres 5652   ∘ ccom 5654  ⟶wf 6535  –1-1-onto→wf1o 6538  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547

This theorem is used by:  f1ocnvfvb  7288  fveqf1o  7311  isocnv  7339  f1oiso2  7361  weniso  7365  dif1enlem  9179  dif1en  9181  ordiso2  9513  cantnfle  9676  cantnfp1lem3  9685  cantnflem1b  9691  cantnflem1d  9693  cantnflem1  9694  cnfcom2lem  9706  cnfcom2  9707  cnfcom3lem  9708  acndom2  10137  iunfictbso  10197  ttukeylem7  10597  fpwwe2lem5  10724  fpwwe2lem6  10725  uzrdglem  14104  uzrdgsuci  14107  fzennn  14115  axdc4uzlem  14130  seqf1olem1  14188  seqf1olem2  14189  hashfz1  14494  seqcoll  14613  seqcoll2  14614  summolem3  15886  summolem2a  15887  ackbijnn  16003  prodmolem3  16106  prodmolem2a  16107  sadcaddlem  16633  sadaddlem  16642  sadasslem  16646  sadeq  16648  phimullem  16962  eulerthlem2  16965  catcisolem  18291  mgmhmf1o  18895  mhmf1o  18997  ghmf1o  19468  f1omvdconj  19666  gsumval3eu  20124  gsumval3  20127  rngisom1  20702  fidomndrnglem  21036  lmhmf1o  21327  basqtop  24036  tgqtop  24037  ordthmeolem  24126  symgtgp  24431  imasf1obl  24813  xrhmeo  25273  ovoliunlem2  25830  vitalilem2  25936  dvcnvlem  26302  dvcnv  26303  dvcnvre  26345  efif1olem4  26879  eff1olem  26882  eflog  26910  dvrelog  26971  dvlog  26985  asinrebnd  27235  sqff1o  27515  lgsqrlem4  27682  addonbday  28671  noseqrdglem  28697  noseqrdgsuc  28700  bdayfinlem  28878  cnvmot  29010  f1otrg  29454  f1otrge  29455  axcontlem10  29557  usgrnbcnvfv  29952  wlkiswwlks2lem4  30467  clwlkclwwlklem2a4  30594  cnvunop  32526  unopadj  32527  bracnvbra  32721  ccatws1f1o  33561  mndlactf1o  33638  mndractf1o  33639  abliso  33643  cycpmco2lem4  33737  cycpmco2lem5  33738  cycpmco2lem6  33739  cycpmco2lem7  33740  cycpmco2  33741  mndpluscn  34605  vonf1oonfo  35969  cvmfolem  36131  cvmliftlem6  36142  f1ocan1fv  38754  ismtycnv  38830  ismtyima  38831  ismtybndlem  38834  rngoisocnv  39009  lautcnvle  41240  lautcvr  41243  lautj  41244  lautm  41245  ltrncnvatb  41289  ltrncnvel  41293  ltrncnv  41297  ltrneq2  41299  cdlemg17h  41819  diainN  42208  diasslssN  42210  doca3N  42278  dihcnvid2  42424  dochocss  42517  mapdcnvid2  42808  sticksstones19  43309  rmxyval  44016  brpermmodelcnv  46088  permaxrep  46090  isuspgrim0lem  49085  isuspgrim0  49086  upgrimwlklem3  49091  uhgrimisgrgriclem  49122  clnbgrgrimlem  49125  uspgrlimlem1  49180  uspgrlimlem2  49181  uspgrlimlem3  49182  uspgrlimlem4  49183  grlicsym  49205  imaf1homlem  50317  uptrar  50426