Theorem elfvmptrab1w

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. Version of elfvmptrab1 with a disjoint variable condition, which does not require ax-13 . (Contributed by Alexander van der Vekens, 15-Jul-2018) Avoid ax-13 . (Revised by Gino Giotto, 26-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		elfvmptrab1w.f	$$⊢F=\left(x\in V⟼\left\{y\in ⦋x/m⦌M|\phi \right\}\right)$$
2		elfvmptrab1w.v	$$⊢X\in V\to ⦋X/m⦌M\in \mathrm{V}$$
3		elfvdm	$$⊢Y\in F\left(X\right)\to X\in \mathrm{dom}F$$
4	1	dmmptss	$$⊢\mathrm{dom}F\subseteq V$$
5	4	sseli	$$⊢X\in \mathrm{dom}F\to X\in V$$
6		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}$$
7	5 2 6	3syl	$$⊢X\in \mathrm{dom}F\to \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
9		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}xM$$
11	8 10	nfcsbw	$$⊢\underset{\_}{Ⅎ}x⦋X/m⦌M$$
12	9 11	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}$$
13		csbeq1	$$⊢x=X\to ⦋x/m⦌M=⦋X/m⦌M$$
14		sbceq1a	$$⊢x=X\to \left(\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right)$$
15	13 14	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\}$$
16	8 12 15 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\}$$
17	5 7 16	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\}$$
18	17	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)$$
19		elrabi	$$⊢Y\in \left\{y\in ⦋X/m⦌M|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\phi \right\}\to Y\in ⦋X/m⦌M$$
20	5 19	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)$$
21	20	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)$$
22	18 21	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)$$
23	3 22	mpcom	$$⊢Y\in F\left(X\right)\to \left(X\in V\wedge Y\in ⦋X/m⦌M\right)$$