Theorem mptrcl 6605

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

Step	Hyp	Ref	Expression
1		n0i 4187	. 2 ⊢ (𝐼 ∈ (𝐹‘𝑋) → ¬ (𝐹‘𝑋) = ∅)
2		mptrcl.1	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
3	2	dmmptss 5936	. . . 4 ⊢ dom 𝐹 ⊆ 𝐴
4	3	sseli 3856	. . 3 ⊢ (𝑋 ∈ dom 𝐹 → 𝑋 ∈ 𝐴)
5		ndmfv 6531	. . 3 ⊢ (¬ 𝑋 ∈ dom 𝐹 → (𝐹‘𝑋) = ∅)
6	4, 5	nsyl4 158	. 2 ⊢ (¬ (𝐹‘𝑋) = ∅ → 𝑋 ∈ 𝐴)
7	1, 6	syl 17	1 ⊢ (𝐼 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ∈ wcel 2050  ∅c0 4180   ↦ cmpt 5009  dom cdm 5408  ‘cfv 6190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-xp 5414  df-rel 5415  df-cnv 5416  df-dm 5418  df-rn 5419  df-res 5420  df-ima 5421  df-iota 6154  df-fv 6198

This theorem is referenced by:  bitsval  15636  subcrcl  16947  initorcl  17115  termorcl  17116  zeroorcl  17117  submrcl  17817  issubg  18066  isnsg  18095  issubrg  19261  issdrg  19299  abvrcl  19317  isobs  20569  islocfin  21832  kgeni  21852  elmptrab  22142  isphtpc  23304  cfili  23577  cfilfcls  23583  plybss  24490  eleenn  26388