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 mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.) |
Ref | Expression |
---|---|
fimacnv | ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imassrn 5934 | . . 3 ⊢ (◡𝐹 “ 𝐵) ⊆ ran ◡𝐹 | |
2 | dfdm4 5758 | . . . 4 ⊢ dom 𝐹 = ran ◡𝐹 | |
3 | fdm 6516 | . . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
4 | ssid 3988 | . . . . 5 ⊢ 𝐴 ⊆ 𝐴 | |
5 | 3, 4 | eqsstrdi 4020 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 ⊆ 𝐴) |
6 | 2, 5 | eqsstrrid 4015 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran ◡𝐹 ⊆ 𝐴) |
7 | 1, 6 | sstrid 3977 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) ⊆ 𝐴) |
8 | fimass 6549 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → (𝐹 “ 𝐴) ⊆ 𝐵) | |
9 | ffun 6511 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → Fun 𝐹) | |
10 | 4, 3 | sseqtrrid 4019 | . . . 4 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 ⊆ dom 𝐹) |
11 | funimass3 6817 | . . . 4 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) | |
12 | 9, 10, 11 | syl2anc 584 | . . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹 “ 𝐴) ⊆ 𝐵 ↔ 𝐴 ⊆ (◡𝐹 “ 𝐵))) |
13 | 8, 12 | mpbid 233 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐴 ⊆ (◡𝐹 “ 𝐵)) |
14 | 7, 13 | eqssd 3983 | 1 ⊢ (𝐹:𝐴⟶𝐵 → (◡𝐹 “ 𝐵) = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ⊆ wss 3935 ◡ccnv 5548 dom cdm 5549 ran crn 5550 “ cima 5552 Fun wfun 6343 ⟶wf 6345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2618 df-eu 2650 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 3497 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-fv 6357 |
This theorem is referenced by: fimacnvinrn 6833 fmpt 6867 frnsuppeq 7833 fin1a2lem7 9817 cnclima 21806 iscncl 21807 cnindis 21830 cncmp 21930 ptrescn 22177 qtopuni 22240 qtopcld 22251 qtopcmap 22257 ordthmeolem 22339 rnelfmlem 22490 mbfdm 24156 ismbf 24158 mbfimaicc 24161 ismbf2d 24170 ismbf3d 24184 mbfimaopn2 24187 i1fd 24211 plyeq0 24730 fsumcvg4 31093 zrhunitpreima 31119 imambfm 31420 carsggect 31476 dstrvprob 31629 poimirlem30 34804 dvtan 34824 smfresal 42944 |
Copyright terms: Public domain | W3C validator |