This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 nfrexw 
 |-  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 nfrexw 
 |-  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 ) )