Theorem f1ocnvfv1 7282

Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)

Assertion

Ref	Expression
f1ocnvfv1	⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶)

Proof of Theorem f1ocnvfv1

Step	Hyp	Ref	Expression
1		f1ococnv1 6852	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴))
2	1	fveq1d 6885	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶))
4		f1of 6822	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
5		fvco3 6983	. . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶)))
6	4, 5	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶)))
7		fvresi 7176	. . 3 ⊢ (𝐶 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐶) = 𝐶)
8	7	adantl 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (( I ↾ 𝐴)‘𝐶) = 𝐶)
9	3, 6, 8	3eqtr3d 2804	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   I cid 5545  ^◡ccnv 5650   ↾ cres 5653   ∘ ccom 5655  ⟶wf 6533  –1-1-onto→wf1o 6536  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545

This theorem is used by:  f1ocnvfv  7284  wemapwe  9691  fseqenlem2  10097  acndom  10123  isf34lem5  10449  axcc3  10509  pwfseqlem1  10736  hashdom  14516  fz1isolem  14599  cnrecnv  15325  sadcadd  16621  sadadd2  16623  invinv  17938  catcisolem  18278  mhmf1o  18984  rngisom1  20689  srngnvl  21100  mdetleib2  22896  2ndcdisj  23768  cnheiborlem  25268  iunmbl2  25871  dvcnvlem  26289  eff1olem  26869  logef  26902  adjbdlnb  32679  cnvbrabra  32707  fsumiunle  33413  ccatws1f1o  33507  fzto1stinvn  33658  cycpmfv1  33667  cycpmfv2  33668  cycpmco2lem7  33686  ricdomn1  33843  madjusmdetlem1  34452  tpr2rico  34537  esumiun  34719  lautj  41130  lautm  41131  ldilcnv  41152  ltrneq2  41185  trlcnv  41202  diaocN  42162  dihcnvid1  42309  dochocss  42403  mapdcnvid1N  42691  aks6d1c1p3  43140  sticksstones19  43195  nvocnvb  44407  grimcnv  48955  gricushgr  48984  uspgrlimlem2  49056