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

Theorem fimacnv 6573
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 5694 . . 3 (𝐹𝐵) ⊆ ran 𝐹
2 dfdm4 5519 . . . 4 dom 𝐹 = ran 𝐹
3 fdm 6264 . . . . 5 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
4 ssid 3819 . . . . 5 𝐴𝐴
53, 4syl6eqss 3851 . . . 4 (𝐹:𝐴𝐵 → dom 𝐹𝐴)
62, 5syl5eqssr 3846 . . 3 (𝐹:𝐴𝐵 → ran 𝐹𝐴)
71, 6syl5ss 3809 . 2 (𝐹:𝐴𝐵 → (𝐹𝐵) ⊆ 𝐴)
8 imassrn 5694 . . . 4 (𝐹𝐴) ⊆ ran 𝐹
9 frn 6262 . . . 4 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
108, 9syl5ss 3809 . . 3 (𝐹:𝐴𝐵 → (𝐹𝐴) ⊆ 𝐵)
11 ffun 6259 . . . 4 (𝐹:𝐴𝐵 → Fun 𝐹)
124, 3syl5sseqr 3850 . . . 4 (𝐹:𝐴𝐵𝐴 ⊆ dom 𝐹)
13 funimass3 6559 . . . 4 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))
1411, 12, 13syl2anc 580 . . 3 (𝐹:𝐴𝐵 → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))
1510, 14mpbid 224 . 2 (𝐹:𝐴𝐵𝐴 ⊆ (𝐹𝐵))
167, 15eqssd 3815 1 (𝐹:𝐴𝐵 → (𝐹𝐵) = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  wss 3769  ccnv 5311  dom cdm 5312  ran crn 5313  cima 5315  Fun wfun 6095  wf 6097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pr 5097
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109
This theorem is referenced by:  fimacnvinrn  6574  fmpt  6606  frnsuppeq  7544  fin1a2lem7  9516  cnclima  21401  iscncl  21402  cnindis  21425  cncmp  21524  ptrescn  21771  qtopuni  21834  qtopcld  21845  qtopcmap  21851  ordthmeolem  21933  rnelfmlem  22084  mbfdm  23734  ismbf  23736  mbfimaicc  23739  ismbf2d  23748  ismbf3d  23762  mbfimaopn2  23765  i1fd  23789  plyeq0  24308  fsumcvg4  30512  zrhunitpreima  30538  imambfm  30840  carsggect  30896  dstrvprob  31050  poimirlem30  33928  dvtan  33948  smfresal  41741
  Copyright terms: Public domain W3C validator