Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fimacnv | Structured version Visualization version GIF version |
Description: The preimage of the codomain of a function is the function's domain. (Contributed by FL, 25-Jan-2007.) (Proof shortened by AV, 20-Sep-2024.) |
Ref | Expression |
---|---|
fimacnv | ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frn 6552 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) | |
2 | cnvimassrndm 6015 | . . 3 ⊢ (ran 𝐹 ⊆ 𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = dom 𝐹) |
4 | fdm 6554 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
5 | 3, 4 | eqtrd 2777 | 1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ⊆ wss 3866 ◡ccnv 5550 dom cdm 5551 ran crn 5552 “ cima 5554 ⟶wf 6376 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-xp 5557 df-cnv 5559 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-fn 6383 df-f 6384 |
This theorem is referenced by: fco 6569 f1co 6627 fimacnvinrn 6892 fmpt 6927 frnsuppeq 7917 frnsuppeqg 7918 fin1a2lem7 10020 cnclima 22165 iscncl 22166 cnindis 22189 cncmp 22289 ptrescn 22536 qtopuni 22599 qtopcld 22610 qtopcmap 22616 ordthmeolem 22698 rnelfmlem 22849 mbfdm 24523 ismbf 24525 mbfimaicc 24528 ismbf2d 24537 ismbf3d 24551 mbfimaopn2 24554 i1fd 24578 plyeq0 25105 elrspunidl 31320 fsumcvg4 31614 zrhunitpreima 31640 imambfm 31941 carsggect 31997 dstrvprob 32150 poimirlem30 35544 dvtan 35564 smfresal 43994 cnneiima 45883 |
Copyright terms: Public domain | W3C validator |