Theorem abrexdomjm

Description: An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypothesis	abrexdomjm.1	$$⊢y\in A\to {\exists }^{*}x\phi$$
Assertion	abrexdomjm	$$⊢A\in V\to \left\{x|\exists y\in A\phi \right\}\preccurlyeq A$$

Proof

Step	Hyp	Ref	Expression
1		abrexdomjm.1	$$⊢y\in A\to {\exists }^{*}x\phi$$
2		df-rex	$$⊢\exists y\in A\phi \leftrightarrow \exists y\left(y\in A\wedge \phi \right)$$
3	2	abbii	$$⊢\left\{x|\exists y\in A\phi \right\}=\left\{x|\exists y\left(y\in A\wedge \phi \right)\right\}$$
4		rnopab	$$⊢\mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}=\left\{x|\exists y\left(y\in A\wedge \phi \right)\right\}$$
5	3 4	eqtr4i	$$⊢\left\{x|\exists y\in A\phi \right\}=\mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
6		dmopabss	$$⊢\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\subseteq A$$
7		ssexg	$$⊢\left(\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\subseteq A\wedge A\in V\right)\to \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
8	6 7	mpan	$$⊢A\in V\to \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\in \mathrm{V}$$
9		funopab	$$⊢\mathrm{Fun}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\leftrightarrow \forall y{\exists }^{*}x\left(y\in A\wedge \phi \right)$$
10		moanimv	$$⊢{\exists }^{*}x\left(y\in A\wedge \phi \right)\leftrightarrow \left(y\in A\to {\exists }^{*}x\phi \right)$$
11	1 10	mpbir	$$⊢{\exists }^{*}x\left(y\in A\wedge \phi \right)$$
12	9 11	mpgbir	$$⊢\mathrm{Fun}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
13	12	a1i	$$⊢A\in V\to \mathrm{Fun}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
14		funfn	$$⊢\mathrm{Fun}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\leftrightarrow \left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}Fn\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
15	13 14	sylib	$$⊢A\in V\to \left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}Fn\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
16		fnrndomg	$$⊢\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\in \mathrm{V}\to \left(\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}Fn\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\to \mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\right)$$
17	8 15 16	sylc	$$⊢A\in V\to \mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}$$
18		ssdomg	$$⊢A\in V\to \left(\mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\subseteq A\to \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq A\right)$$
19	6 18	mpi	$$⊢A\in V\to \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq A$$
20		domtr	$$⊢\left(\mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\wedge \mathrm{dom}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq A\right)\to \mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq A$$
21	17 19 20	syl2anc	$$⊢A\in V\to \mathrm{ran}\left\{⟨y,x⟩|\left(y\in A\wedge \phi \right)\right\}\preccurlyeq A$$
22	5 21	eqbrtrid	$$⊢A\in V\to \left\{x|\exists y\in A\phi \right\}\preccurlyeq A$$