|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > f1ocnvfv1 | Structured version Visualization version GIF version | ||
| Description: The converse value of the value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) | 
| Ref | Expression | 
|---|---|
| f1ocnvfv1 | ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | f1ococnv1 6876 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴)) | |
| 2 | 1 | fveq1d 6907 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶)) | 
| 3 | 2 | adantr 480 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶)) | 
| 4 | f1of 6847 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
| 5 | fvco3 7007 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶))) | |
| 6 | 4, 5 | sylan 580 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶))) | 
| 7 | fvresi 7194 | . . 3 ⊢ (𝐶 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐶) = 𝐶) | |
| 8 | 7 | adantl 481 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (( I ↾ 𝐴)‘𝐶) = 𝐶) | 
| 9 | 3, 6, 8 | 3eqtr3d 2784 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 ∈ wcel 2107 I cid 5576 ◡ccnv 5683 ↾ cres 5686 ∘ ccom 5688 ⟶wf 6556 –1-1-onto→wf1o 6559 ‘cfv 6560 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-br 5143 df-opab 5205 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 | 
| This theorem is referenced by: f1ocnvfv 7299 wemapwe 9738 fseqenlem2 10066 acndom 10092 isf34lem5 10419 axcc3 10479 pwfseqlem1 10699 hashdom 14419 fz1isolem 14501 cnrecnv 15205 sadcadd 16496 sadadd2 16498 invinv 17815 catcisolem 18156 mhmf1o 18810 rngisom1 20467 srngnvl 20852 mdetleib2 22595 2ndcdisj 23465 cnheiborlem 24987 iunmbl2 25593 dvcnvlem 26015 eff1olem 26591 logef 26624 adjbdlnb 32104 cnvbrabra 32132 fsumiunle 32832 ccatws1f1o 32937 fzto1stinvn 33125 cycpmfv1 33134 cycpmfv2 33135 cycpmco2lem7 33153 madjusmdetlem1 33827 tpr2rico 33912 esumiun 34096 lautj 40096 lautm 40097 ldilcnv 40118 ltrneq2 40151 trlcnv 40168 diaocN 41128 dihcnvid1 41275 dochocss 41369 mapdcnvid1N 41657 aks6d1c1p3 42112 sticksstones19 42167 nvocnvb 43440 grimcnv 47884 gricushgr 47891 uspgrlimlem2 47961 | 
| Copyright terms: Public domain | W3C validator |