MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fimacnv Structured version   Visualization version   GIF version

Theorem fimacnv 6490
Description: The preimage of the codomain of a mapping is the mapping's domain. (Contributed by FL, 25-Jan-2007.)
Assertion
Ref Expression
fimacnv (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)

Proof of Theorem fimacnv
StepHypRef Expression
1 imassrn 5618 . . 3 (𝐹𝐵) ⊆ ran 𝐹
2 dfdm4 5454 . . . 4 dom 𝐹 = ran 𝐹
3 fdm 6191 . . . . 5 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
4 ssid 3773 . . . . 5 𝐴𝐴
53, 4syl6eqss 3804 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
62, 5syl5eqssr 3799 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐴)
71, 6syl5ss 3763 . 2 (𝐹:𝐴𝐵 → (𝐹𝐵) ⊆ 𝐴)
8 imassrn 5618 . . . 4 (𝐹𝐴) ⊆ ran 𝐹
9 frn 6193 . . . 4 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
108, 9syl5ss 3763 . . 3 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
11 ffun 6188 . . . 4 (𝐹:𝐴𝐵 → Fun 𝐹)
124, 3syl5sseqr 3803 . . . 4 (𝐹:𝐴𝐵𝐴 ⊆ dom 𝐹)
13 funimass3 6476 . . . 4 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))
1411, 12, 13syl2anc 565 . . 3 (𝐹:𝐴𝐵 → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))
1510, 14mpbid 222 . 2 (𝐹:𝐴𝐵𝐴 ⊆ (𝐹𝐵))
167, 15eqssd 3769 1 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wss 3723  ccnv 5248  dom cdm 5249  ran crn 5250  cima 5252  Fun wfun 6025  wf 6027
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-fv 6039
This theorem is referenced by:  fimacnvinrn  6491  fmpt  6523  frnsuppeq  7457  fin1a2lem7  9429  cnclima  21292  iscncl  21293  cnindis  21316  cncmp  21415  ptrescn  21662  qtopuni  21725  qtopcld  21736  qtopcmap  21742  ordthmeolem  21824  rnelfmlem  21975  mbfdm  23613  ismbf  23615  mbfimaicc  23618  ismbf2d  23627  ismbf3d  23640  mbfimaopn2  23643  i1fd  23667  plyeq0  24186  fsumcvg4  30333  zrhunitpreima  30359  imambfm  30661  carsggect  30717  dstrvprob  30870  poimirlem30  33768  dvtan  33788  smfresal  41511
  Copyright terms: Public domain W3C validator