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	|- ( ( B e. M /\ A. x e. A E. y e. B ph ) -> E. c ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )

Proof

Step	Hyp	Ref	Expression
1		rabexg	|- ( B e. M -> { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } e. _V )
2		ssrab2	|- { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B
3	2	a1i	|- ( A. x e. A E. y e. B ph -> { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B )
4		nfv	|- F/ y x e. A
5		nfre1	|- F/ y E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph
6		sbceq2a	|- ( w = x -> ( [. w / x ]. ph <-> ph ) )
7	6	rspcev	|- ( ( x e. A /\ ph ) -> E. w e. A [. w / x ]. ph )
8	7	ancoms	|- ( ( ph /\ x e. A ) -> E. w e. A [. w / x ]. ph )
9	8	anim1ci	|- ( ( ( ph /\ x e. A ) /\ y e. B ) -> ( y e. B /\ E. w e. A [. w / x ]. ph ) )
10	9	anasss	|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( y e. B /\ E. w e. A [. w / x ]. ph ) )
11	10	ancoms	|- ( ( ( x e. A /\ y e. B ) /\ ph ) -> ( y e. B /\ E. w e. A [. w / x ]. ph ) )
12		sbceq2a	|- ( z = y -> ( [. z / y ]. ph <-> ph ) )
13	12	sbcbidv	|- ( z = y -> ( [. w / x ]. [. z / y ]. ph <-> [. w / x ]. ph ) )
14	13	rexbidv	|- ( z = y -> ( E. w e. A [. w / x ]. [. z / y ]. ph <-> E. w e. A [. w / x ]. ph ) )
15	14	elrab	|- ( y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } <-> ( y e. B /\ E. w e. A [. w / x ]. ph ) )
16	11 15	sylibr	|- ( ( ( x e. A /\ y e. B ) /\ ph ) -> y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } )
17		sbceq2a	|- ( v = y -> ( [. v / y ]. ph <-> ph ) )
18	17	rspcev	|- ( ( y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } /\ ph ) -> E. v e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } [. v / y ]. ph )
19	16 18	sylancom	|- ( ( ( x e. A /\ y e. B ) /\ ph ) -> E. v e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } [. v / y ]. ph )
20		nfcv	|- F/_ v { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph }
21		nfcv	|- F/_ y A
22		nfcv	|- F/_ y w
23		nfsbc1v	|- F/ y [. z / y ]. ph
24	22 23	nfsbcw	|- F/ y [. w / x ]. [. z / y ]. ph
25	21 24	nfrex	|- F/ y E. w e. A [. w / x ]. [. z / y ]. ph
26		nfcv	|- F/_ y B
27	25 26	nfrabw	|- F/_ y { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph }
28		nfsbc1v	|- F/ y [. v / y ]. ph
29		nfv	|- F/ v ph
30	20 27 28 29 17	cbvrexfw	|- ( E. v e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } [. v / y ]. ph <-> E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph )
31	19 30	sylib	|- ( ( ( x e. A /\ y e. B ) /\ ph ) -> E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph )
32	31	exp31	|- ( x e. A -> ( y e. B -> ( ph -> E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph ) ) )
33	4 5 32	rexlimd	|- ( x e. A -> ( E. y e. B ph -> E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph ) )
34	33	ralimia	|- ( A. x e. A E. y e. B ph -> A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph )
35		nfsbc1v	|- F/ x [. w / x ]. ph
36		nfv	|- F/ w ph
37	35 36 6	cbvrexw	|- ( E. w e. A [. w / x ]. ph <-> E. x e. A ph )
38	14 37	bitrdi	|- ( z = y -> ( E. w e. A [. w / x ]. [. z / y ]. ph <-> E. x e. A ph ) )
39	38	elrab	|- ( y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } <-> ( y e. B /\ E. x e. A ph ) )
40	39	simprbi	|- ( y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> E. x e. A ph )
41	40	rgen	|- A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph
42	41	a1i	|- ( A. x e. A E. y e. B ph -> A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph )
43	3 34 42	3jca	|- ( A. x e. A E. y e. B ph -> ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B /\ A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph /\ A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph ) )
44		sseq1	|- ( c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> ( c C_ B <-> { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B ) )
45		nfcv	|- F/_ x A
46		nfsbc1v	|- F/ x [. w / x ]. [. z / y ]. ph
47	45 46	nfrex	|- F/ x E. w e. A [. w / x ]. [. z / y ]. ph
48		nfcv	|- F/_ x B
49	47 48	nfrabw	|- F/_ x { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph }
50	49	nfeq2	|- F/ x c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph }
51		nfcv	|- F/_ y c
52	51 27	rexeqf	|- ( c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> ( E. y e. c ph <-> E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph ) )
53	50 52	ralbid	|- ( c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> ( A. x e. A E. y e. c ph <-> A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph ) )
54	51 27	raleqf	|- ( c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> ( A. y e. c E. x e. A ph <-> A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph ) )
55	44 53 54	3anbi123d	|- ( c = { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } -> ( ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) <-> ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B /\ A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph /\ A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph ) ) )
56	55	spcegv	|- ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } e. _V -> ( ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B /\ A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph /\ A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph ) -> E. c ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) ) )
57	56	imp	|- ( ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } e. _V /\ ( { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } C_ B /\ A. x e. A E. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } ph /\ A. y e. { z e. B | E. w e. A [. w / x ]. [. z / y ]. ph } E. x e. A ph ) ) -> E. c ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )
58	1 43 57	syl2an	|- ( ( B e. M /\ A. x e. A E. y e. B ph ) -> E. c ( c C_ B /\ A. x e. A E. y e. c ph /\ A. y e. c E. x e. A ph ) )