Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  indexa Structured version   Unicode version

Theorem indexa 28767
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.)
Assertion
Ref Expression
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 ) )
Distinct variable groups:    x, A, y, c    x, B, y, c    ph, c
Allowed substitution hints:    ph( x, y)    M( x, y, c)

Proof of Theorem indexa
Dummy variables  z  w  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rabexg 4542 . 2  |-  ( B  e.  M  ->  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  e.  _V )
2 ssrab2 3537 . . . 4  |-  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  C_  B
32a1i 11 . . 3  |-  ( 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 1674 . . . . 5  |-  F/ y  x  e.  A
5 nfre1 2883 . . . . 5  |-  F/ y E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph
6 sbceq2a 3298 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( [. w  /  x ]. ph  <->  ph ) )
76rspcev 3171 . . . . . . . . . . . . . 14  |-  ( ( x  e.  A  /\  ph )  ->  E. w  e.  A  [. w  /  x ]. ph )
87ancoms 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  E. w  e.  A  [. w  /  x ]. ph )
98anim2i 569 . . . . . . . . . . . 12  |-  ( ( y  e.  B  /\  ( ph  /\  x  e.  A ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
109ancoms 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  (
y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph )
)
1110anasss 647 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
1211ancoms 453 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
13 sbceq2a 3298 . . . . . . . . . . . 12  |-  ( z  =  y  ->  ( [. z  /  y ]. ph  <->  ph ) )
1413sbcbidv 3345 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( [. w  /  x ]. [. z  /  y ]. ph  <->  [. w  /  x ]. ph ) )
1514rexbidv 2848 . . . . . . . . . 10  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. w  e.  A  [. w  /  x ]. ph )
)
1615elrab 3216 . . . . . . . . 9  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  <->  ( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
1712, 16sylibr 212 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
)
18 sbceq2a 3298 . . . . . . . . 9  |-  ( v  =  y  ->  ( [. v  /  y ]. ph  <->  ph ) )
1918rspcev 3171 . . . . . . . 8  |-  ( ( 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 )
2017, 19sylancom 667 . . . . . . 7  |-  ( ( ( 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 )
21 nfcv 2613 . . . . . . . 8  |-  F/_ v { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
22 nfcv 2613 . . . . . . . . . 10  |-  F/_ y A
23 nfcv 2613 . . . . . . . . . . 11  |-  F/_ y
w
24 nfsbc1v 3306 . . . . . . . . . . 11  |-  F/ y
[. z  /  y ]. ph
2523, 24nfsbc 3308 . . . . . . . . . 10  |-  F/ y
[. w  /  x ]. [. z  /  y ]. ph
2622, 25nfrex 2882 . . . . . . . . 9  |-  F/ y E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
27 nfcv 2613 . . . . . . . . 9  |-  F/_ y B
2826, 27nfrab 3000 . . . . . . . 8  |-  F/_ y { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
29 nfsbc1v 3306 . . . . . . . 8  |-  F/ y
[. v  /  y ]. ph
30 nfv 1674 . . . . . . . 8  |-  F/ v
ph
3121, 28, 29, 30, 18cbvrexf 3040 . . . . . . 7  |-  ( 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 )
3220, 31sylib 196 . . . . . 6  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  ->  E. y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph )
3332exp31 604 . . . . 5  |-  ( x  e.  A  ->  (
y  e.  B  -> 
( ph  ->  E. y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph ) ) )
344, 5, 33rexlimd 2936 . . . 4  |-  ( x  e.  A  ->  ( E. y  e.  B  ph 
->  E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph ) )
3534ralimia 2809 . . 3  |-  ( 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 )
36 nfsbc1v 3306 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
37 nfv 1674 . . . . . . . . 9  |-  F/ w ph
3836, 37, 6cbvrex 3042 . . . . . . . 8  |-  ( E. w  e.  A  [. w  /  x ]. ph  <->  E. x  e.  A  ph )
3915, 38syl6bb 261 . . . . . . 7  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. x  e.  A  ph ) )
4039elrab 3216 . . . . . 6  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  <->  ( y  e.  B  /\  E. x  e.  A  ph ) )
4140simprbi 464 . . . . 5  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  ->  E. x  e.  A  ph )
4241rgen 2891 . . . 4  |-  A. y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } E. x  e.  A  ph
4342a1i 11 . . 3  |-  ( 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 )
443, 35, 433jca 1168 . 2  |-  ( 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 ) )
45 sseq1 3477 . . . . 5  |-  ( 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 ) )
46 nfcv 2613 . . . . . . . . 9  |-  F/_ x A
47 nfsbc1v 3306 . . . . . . . . 9  |-  F/ x [. w  /  x ]. [. z  /  y ]. ph
4846, 47nfrex 2882 . . . . . . . 8  |-  F/ x E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
49 nfcv 2613 . . . . . . . 8  |-  F/_ x B
5048, 49nfrab 3000 . . . . . . 7  |-  F/_ x { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
5150nfeq2 2629 . . . . . 6  |-  F/ x  c  =  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
52 nfcv 2613 . . . . . . 7  |-  F/_ y
c
5352, 28rexeqf 3012 . . . . . 6  |-  ( 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 ) )
5451, 53ralbid 2835 . . . . 5  |-  ( 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 ) )
5552, 28raleqf 3011 . . . . 5  |-  ( 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 ) )
5645, 54, 553anbi123d 1290 . . . 4  |-  ( 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 ) ) )
5756spcegv 3156 . . 3  |-  ( { 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 ) ) )
5857imp 429 . 2  |-  ( ( { 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 ) )
591, 44, 58syl2an 477 1  |-  ( ( 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 ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1370   E.wex 1587    e. wcel 1758   A.wral 2795   E.wrex 2796   {crab 2799   _Vcvv 3070   [.wsbc 3286    C_ wss 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-sbc 3287  df-in 3435  df-ss 3442
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator