Theorem indexa

Description: If for every element of an indexing set A there exists a corresponding element of another set B , then there exists a subset of B consisting only of those elements which are indexed by A . Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	indexa	$$⊢\left(B\in M\wedge \forall x\in A\exists y\in B\phi \right)\to \exists c\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		rabexg	$$⊢B\in M\to \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
2		ssrab2	$$⊢\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B$$
3	2	a1i	$$⊢\forall x\in A\exists y\in B\phi \to \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B$$
4		nfv	$$⊢Ⅎyx\in A$$
5		nfre1	$$⊢Ⅎy\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi$$
6		sbceq2a	$$⊢w=x\to \left(\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
7	6	rspcev	$$⊢\left(x\in A\wedge \phi \right)\to \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi$$
8	7	ancoms	$$⊢\left(\phi \wedge x\in A\right)\to \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi$$
9	8	anim1ci	$$⊢\left(\left(\phi \wedge x\in A\right)\wedge y\in B\right)\to \left(y\in B\wedge \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
10	9	anasss	$$⊢\left(\phi \wedge \left(x\in A\wedge y\in B\right)\right)\to \left(y\in B\wedge \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
11	10	ancoms	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\to \left(y\in B\wedge \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
12		sbceq2a	$$⊢z=y\to \left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
13	12	sbcbidv	$$⊢z=y\to \left(\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
14	13	rexbidv	$$⊢z=y\to \left(\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
15	14	elrab	$$⊢y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(y\in B\wedge \exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \right)$$
16	11 15	sylibr	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\to y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}$$
17		sbceq2a	$$⊢v=y\to \left(\underset{\dot{}}{[}v/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
18	17	rspcev	$$⊢\left(y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\wedge \phi \right)\to \exists v\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\underset{\dot{}}{[}v/y\underset{\dot{}}{]}\phi$$
19	16 18	sylancom	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\to \exists v\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\underset{\dot{}}{[}v/y\underset{\dot{}}{]}\phi$$
20		nfcv	$$⊢\underset{\_}{Ⅎ}v\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}yw$$
23		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
24	22 23	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
25	21 24	nfrexw	$$⊢Ⅎy\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
27	25 26	nfrabw	$$⊢\underset{\_}{Ⅎ}y\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}$$
28		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}v/y\underset{\dot{}}{]}\phi$$
29		nfv	$$⊢Ⅎv\phi$$
30	20 27 28 29 17	cbvrexfw	$$⊢\exists v\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\underset{\dot{}}{[}v/y\underset{\dot{}}{]}\phi \leftrightarrow \exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi$$
31	19 30	sylib	$$⊢\left(\left(x\in A\wedge y\in B\right)\wedge \phi \right)\to \exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi$$
32	31	exp31	$$⊢x\in A\to \left(y\in B\to \left(\phi \to \exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \right)\right)$$
33	4 5 32	rexlimd	$$⊢x\in A\to \left(\exists y\in B\phi \to \exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \right)$$
34	33	ralimia	$$⊢\forall x\in A\exists y\in B\phi \to \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi$$
35		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi$$
36		nfv	$$⊢Ⅎw\phi$$
37	35 36 6	cbvrexw	$$⊢\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\phi \leftrightarrow \exists x\in A\phi$$
38	14 37	bitrdi	$$⊢z=y\to \left(\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \leftrightarrow \exists x\in A\phi \right)$$
39	38	elrab	$$⊢y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(y\in B\wedge \exists x\in A\phi \right)$$
40	39	simprbi	$$⊢y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \exists x\in A\phi$$
41	40	rgen	$$⊢\forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi$$
42	41	a1i	$$⊢\forall x\in A\exists y\in B\phi \to \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi$$
43	3 34 42	3jca	$$⊢\forall x\in A\exists y\in B\phi \to \left(\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B\wedge \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \wedge \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi \right)$$
44		sseq1	$$⊢c=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \left(c\subseteq B\leftrightarrow \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B\right)$$
45		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
46		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
47	45 46	nfrexw	$$⊢Ⅎx\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi$$
48		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
49	47 48	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}$$
50	49	nfeq2	$$⊢Ⅎxc=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}$$
51		nfcv	$$⊢\underset{\_}{Ⅎ}yc$$
52	51 27	rexeqf	$$⊢c=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \left(\exists y\in c\phi \leftrightarrow \exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \right)$$
53	50 52	ralbid	$$⊢c=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \left(\forall x\in A\exists y\in c\phi \leftrightarrow \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \right)$$
54	51 27	raleqf	$$⊢c=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \left(\forall y\in c\exists x\in A\phi \leftrightarrow \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi \right)$$
55	44 53 54	3anbi123d	$$⊢c=\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\to \left(\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)\leftrightarrow \left(\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B\wedge \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \wedge \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi \right)\right)$$
56	55	spcegv	$$⊢\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}\to \left(\left(\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B\wedge \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \wedge \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi \right)\to \exists c\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)\right)$$
57	56	imp	$$⊢\left(\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}\wedge \left(\left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\subseteq B\wedge \forall x\in A\exists y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\phi \wedge \forall y\in \left\{z\in B|\exists w\in A\underset{\dot{}}{[}w/x\underset{\dot{}}{]}\underset{\dot{}}{[}z/y\underset{\dot{}}{]}\phi \right\}\exists x\in A\phi \right)\right)\to \exists c\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$
58	1 43 57	syl2an	$$⊢\left(B\in M\wedge \forall x\in A\exists y\in B\phi \right)\to \exists c\left(c\subseteq B\wedge \forall x\in A\exists y\in c\phi \wedge \forall y\in c\exists x\in A\phi \right)$$