Theorem f1ocnvfv2 7036

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 6643	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6674	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 483	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6629	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6617	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6762	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 582	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 6937	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 484	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2866	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   I cid 5461  ^◡ccnv 5556   ↾ cres 5559   ∘ ccom 5561  ⟶wf 6353  –1-1-onto→wf1o 6356  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365

This theorem is referenced by:  f1ocnvfvb  7038  fveqf1o  7060  isocnv  7085  f1oiso2  7107  weniso  7109  ordiso2  8981  cantnfle  9136  cantnfp1lem3  9145  cantnflem1b  9151  cantnflem1d  9153  cantnflem1  9154  cnfcom2lem  9166  cnfcom2  9167  cnfcom3lem  9168  acndom2  9482  iunfictbso  9542  ttukeylem7  9939  fpwwe2lem6  10059  fpwwe2lem7  10060  uzrdglem  13328  uzrdgsuci  13331  fzennn  13339  axdc4uzlem  13354  seqf1olem1  13412  seqf1olem2  13413  hashfz1  13709  seqcoll  13825  seqcoll2  13826  summolem3  15073  summolem2a  15074  ackbijnn  15185  prodmolem3  15289  prodmolem2a  15290  sadcaddlem  15808  sadaddlem  15817  sadasslem  15821  sadeq  15823  phimullem  16118  eulerthlem2  16121  catcisolem  17368  mhmf1o  17968  ghmf1o  18390  f1omvdconj  18576  gsumval3eu  19026  gsumval3  19029  lmhmf1o  19820  fidomndrnglem  20081  basqtop  22321  tgqtop  22322  ordthmeolem  22411  symgtgp  22716  imasf1obl  23100  xrhmeo  23552  ovoliunlem2  24106  vitalilem2  24212  dvcnvlem  24575  dvcnv  24576  dvcnvre  24618  efif1olem4  25131  eff1olem  25134  eflog  25162  dvrelog  25222  dvlog  25236  asinrebnd  25481  sqff1o  25761  lgsqrlem4  25927  cnvmot  26329  f1otrg  26659  f1otrge  26660  axcontlem10  26761  usgrnbcnvfv  27149  wlkiswwlks2lem4  27652  clwlkclwwlklem2a4  27777  cnvunop  29697  unopadj  29698  bracnvbra  29892  abliso  30685  cycpmco2lem4  30773  cycpmco2lem5  30774  cycpmco2lem6  30775  cycpmco2lem7  30776  cycpmco2  30777  mndpluscn  31171  cvmfolem  32528  cvmliftlem6  32539  f1ocan1fv  35003  ismtycnv  35082  ismtyima  35083  ismtybndlem  35086  rngoisocnv  35261  lautcnvle  37227  lautcvr  37230  lautj  37231  lautm  37232  ltrncnvatb  37276  ltrncnvel  37280  ltrncnv  37284  ltrneq2  37286  cdlemg17h  37806  diainN  38195  diasslssN  38197  doca3N  38265  dihcnvid2  38411  dochocss  38504  mapdcnvid2  38795  rmxyval  39519  isomgrsym  44008  mgmhmf1o  44061