Theorem elfvmptrab1

Description: Implications for the value of a function defined by the maps-to notation with a class abstraction as a result having an element. Here, the base set of the class abstraction depends on the argument of the function. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker elfvmptrab1w when possible. (Contributed by Alexander van der Vekens, 15-Jul-2018) (New usage is discouraged.)

	Ref	Expression
Hypotheses	elfvmptrab1.f	$$⊢F=\left(x\in V⟼\left\{y\in ⦋x/m⦌M|\phi \right\}\right)$$
	elfvmptrab1.v	$$⊢X\in V\to ⦋X/m⦌M\in \mathrm{V}$$
Assertion	elfvmptrab1	$$⊢Y\in F\left(X\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab1.f	$$⊢F=\left(x\in V⟼\left\{y\in ⦋x/m⦌M|\phi \right\}\right)$$
2		elfvmptrab1.v	$$⊢X\in V\to ⦋X/m⦌M\in \mathrm{V}$$
3		ne0i	$$⊢Y\in F\left(X\right)\to F\left(X\right)\ne \varnothing$$
4		ndmfv	$$⊢\neg X\in \mathrm{dom}F\to F\left(X\right)=\varnothing$$
5	4	necon1ai	$$⊢F\left(X\right)\ne \varnothing \to X\in \mathrm{dom}F$$
6	1	dmmptss	$$⊢\mathrm{dom}F\subseteq V$$
7	6	sseli	$$⊢X\in \mathrm{dom}F\to X\in V$$
8		rabexg	$$⊢⦋X/m⦌M\in \mathrm{V}\to \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
9	7 2 8	3syl	$$⊢X\in \mathrm{dom}F\to \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
11		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xM$$
13	10 12	nfcsb	$$⊢\underset{\_}{Ⅎ}x⦋X/m⦌M$$
14	11 13	nfrab	$$⊢\underset{\_}{Ⅎ}x\left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}$$
15		csbeq1	$$⊢x=X\to ⦋x/m⦌M=⦋X/m⦌M$$
16		sbceq1a	$$⊢x=X\to \left(\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right)$$
17	15 16	rabeqbidv	$$⊢x=X\to \left\{y\in ⦋x/m⦌M|\phi \right\}=\left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}$$
18	10 14 17 1	fvmptf	$$⊢\left(X\in V\wedge \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}\right)\to F\left(X\right)=\left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}$$
19	7 9 18	syl2anc	$$⊢X\in \mathrm{dom}F\to F\left(X\right)=\left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}$$
20	19	eleq2d	$$⊢X\in \mathrm{dom}F\to \left(Y\in F\left(X\right)\leftrightarrow Y\in \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\right)$$
21		elrabi	$$⊢Y\in \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\to Y\in ⦋X/m⦌M$$
22	7 21	anim12i	$$⊢\left(X\in \mathrm{dom}F\wedge Y\in \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)$$
23	22	ex	$$⊢X\in \mathrm{dom}F\to \left(Y\in \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)\right)$$
24	20 23	sylbid	$$⊢X\in \mathrm{dom}F\to \left(Y\in F\left(X\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)\right)$$
25	3 5 24	3syl	$$⊢Y\in F\left(X\right)\to \left(Y\in F\left(X\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)\right)$$
26	25	pm2.43i	$$⊢Y\in F\left(X\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)$$