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	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	mptrcl	$$⊢I\in F\left(X\right)\to X\in A$$

Proof

Step	Hyp	Ref	Expression
1		mptrcl.1	$$⊢F=\left(x\in A⟼B\right)$$
2		n0i	$$⊢I\in F\left(X\right)\to \neg F\left(X\right)=\varnothing$$
3	1	dmmptss	$$⊢\mathrm{dom}F\subseteq A$$
4	3	sseli	$$⊢X\in \mathrm{dom}F\to X\in A$$
5		ndmfv	$$⊢\neg X\in \mathrm{dom}F\to F\left(X\right)=\varnothing$$
6	4 5	nsyl4	$$⊢\neg F\left(X\right)=\varnothing \to X\in A$$
7	2 6	syl	$$⊢I\in F\left(X\right)\to X\in A$$