![]() |
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 6466 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (◡𝐹 ∘ 𝐹) = ( I ↾ 𝐴)) | |
2 | 1 | fveq1d 6495 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶)) |
3 | 2 | adantr 473 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (( I ↾ 𝐴)‘𝐶)) |
4 | f1of 6438 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) | |
5 | fvco3 6582 | . . 3 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶))) | |
6 | 4, 5 | sylan 572 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → ((◡𝐹 ∘ 𝐹)‘𝐶) = (◡𝐹‘(𝐹‘𝐶))) |
7 | fvresi 6752 | . . 3 ⊢ (𝐶 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐶) = 𝐶) | |
8 | 7 | adantl 474 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (( I ↾ 𝐴)‘𝐶) = 𝐶) |
9 | 3, 6, 8 | 3eqtr3d 2816 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐴) → (◡𝐹‘(𝐹‘𝐶)) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 = wceq 1507 ∈ wcel 2050 I cid 5305 ◡ccnv 5400 ↾ cres 5403 ∘ ccom 5405 ⟶wf 6178 –1-1-onto→wf1o 6181 ‘cfv 6182 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3676 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-id 5306 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 |
This theorem is referenced by: f1ocnvfv 6854 wemapwe 8948 fseqenlem2 9239 acndom 9265 isf34lem5 9592 axcc3 9652 pwfseqlem1 9872 hashdom 13547 fz1isolem 13626 cnrecnv 14379 sadcadd 15661 sadadd2 15663 invinv 16892 catcisolem 17218 mhmf1o 17807 srngnvl 19343 mdetleib2 20895 2ndcdisj 21762 cnheiborlem 23255 iunmbl2 23855 dvcnvlem 24270 eff1olem 24827 logef 24860 adjbdlnb 29636 cnvbrabra 29664 fsumiunle 30292 cycpmfv1 30449 cycpmfv2 30450 fzto1stinvn 30695 madjusmdetlem1 30734 tpr2rico 30799 esumiun 30997 lautj 36674 lautm 36675 ldilcnv 36696 ltrneq2 36729 trlcnv 36746 diaocN 37706 dihcnvid1 37853 dochocss 37947 mapdcnvid1N 38235 isomushgr 43359 |
Copyright terms: Public domain | W3C validator |