Theorem f1ocnvfv2 7034

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 6641	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6672	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 483	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6627	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6615	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6760	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 582	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 6935	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 484	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2864	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   I cid 5459  ^◡ccnv 5554   ↾ cres 5557   ∘ ccom 5559  ⟶wf 6351  –1-1-onto→wf1o 6354  ‘cfv 6355

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 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363

This theorem is referenced by:  f1ocnvfvb  7036  fveqf1o  7058  isocnv  7083  f1oiso2  7105  weniso  7107  ordiso2  8979  cantnfle  9134  cantnfp1lem3  9143  cantnflem1b  9149  cantnflem1d  9151  cantnflem1  9152  cnfcom2lem  9164  cnfcom2  9165  cnfcom3lem  9166  acndom2  9480  iunfictbso  9540  ttukeylem7  9937  fpwwe2lem6  10057  fpwwe2lem7  10058  uzrdglem  13326  uzrdgsuci  13329  fzennn  13337  axdc4uzlem  13352  seqf1olem1  13410  seqf1olem2  13411  hashfz1  13707  seqcoll  13823  seqcoll2  13824  summolem3  15071  summolem2a  15072  ackbijnn  15183  prodmolem3  15287  prodmolem2a  15288  sadcaddlem  15806  sadaddlem  15815  sadasslem  15819  sadeq  15821  phimullem  16116  eulerthlem2  16119  catcisolem  17366  mhmf1o  17966  ghmf1o  18388  f1omvdconj  18574  gsumval3eu  19024  gsumval3  19027  lmhmf1o  19818  fidomndrnglem  20079  basqtop  22319  tgqtop  22320  ordthmeolem  22409  symgtgp  22714  imasf1obl  23098  xrhmeo  23550  ovoliunlem2  24104  vitalilem2  24210  dvcnvlem  24573  dvcnv  24574  dvcnvre  24616  efif1olem4  25129  eff1olem  25132  eflog  25160  dvrelog  25220  dvlog  25234  asinrebnd  25479  sqff1o  25759  lgsqrlem4  25925  cnvmot  26327  f1otrg  26657  f1otrge  26658  axcontlem10  26759  usgrnbcnvfv  27147  wlkiswwlks2lem4  27650  clwlkclwwlklem2a4  27775  cnvunop  29695  unopadj  29696  bracnvbra  29890  abliso  30683  cycpmco2lem4  30771  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmco2  30775  mndpluscn  31169  cvmfolem  32526  cvmliftlem6  32537  f1ocan1fv  35016  ismtycnv  35095  ismtyima  35096  ismtybndlem  35099  rngoisocnv  35274  lautcnvle  37240  lautcvr  37243  lautj  37244  lautm  37245  ltrncnvatb  37289  ltrncnvel  37293  ltrncnv  37297  ltrneq2  37299  cdlemg17h  37819  diainN  38208  diasslssN  38210  doca3N  38278  dihcnvid2  38424  dochocss  38517  mapdcnvid2  38808  rmxyval  39532  isomgrsym  44021  mgmhmf1o  44074