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

Theorem mptrcl 6764
 Description: Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.)
Hypothesis
Ref Expression
mptrcl.1 𝐹 = (𝑥𝐴𝐵)
Assertion
Ref Expression
mptrcl (𝐼 ∈ (𝐹𝑋) → 𝑋𝐴)
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝐼(𝑥)   𝑋(𝑥)

Proof of Theorem mptrcl
StepHypRef Expression
1 n0i 4252 . 2 (𝐼 ∈ (𝐹𝑋) → ¬ (𝐹𝑋) = ∅)
2 mptrcl.1 . . . . 5 𝐹 = (𝑥𝐴𝐵)
32dmmptss 6067 . . . 4 dom 𝐹𝐴
43sseli 3913 . . 3 (𝑋 ∈ dom 𝐹𝑋𝐴)
5 ndmfv 6685 . . 3 𝑋 ∈ dom 𝐹 → (𝐹𝑋) = ∅)
64, 5nsyl4 161 . 2 (¬ (𝐹𝑋) = ∅ → 𝑋𝐴)
71, 6syl 17 1 (𝐼 ∈ (𝐹𝑋) → 𝑋𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111  ∅c0 4246   ↦ cmpt 5114  dom cdm 5523  ‘cfv 6332 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-xp 5529  df-rel 5530  df-cnv 5531  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6291  df-fv 6340 This theorem is referenced by:  bitsval  15783  subcrcl  17098  initorcl  17266  termorcl  17267  zeroorcl  17268  submrcl  17979  issubg  18292  isnsg  18320  issubrg  19549  issdrg  19588  abvrcl  19606  isobs  20431  islocfin  22163  kgeni  22183  elmptrab  22473  isphtpc  23640  cfili  23913  cfilfcls  23919  plybss  24835  eleenn  26734
 Copyright terms: Public domain W3C validator