This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mptrcl

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)

		Ref	Expression
	Hypothesis	mptrcl.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	Assertion	mptrcl	⊢ ( 𝐼 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝐴 )

Proof

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