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

Theorem indexa 26412
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 4164 . 2  |-  ( B  e.  M  ->  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  e.  _V )
2 ssrab2 3258 . . . 4  |-  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  C_  B
32a1i 10 . . 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 1605 . . . . 5  |-  F/ y  x  e.  A
5 nfre1 2599 . . . . 5  |-  F/ y E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph
6 sbceq2a 3002 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( [. w  /  x ]. ph  <->  ph ) )
76rspcev 2884 . . . . . . . . . . . . . 14  |-  ( ( x  e.  A  /\  ph )  ->  E. w  e.  A  [. w  /  x ]. ph )
87ancoms 439 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  E. w  e.  A  [. w  /  x ]. ph )
98anim2i 552 . . . . . . . . . . . 12  |-  ( ( y  e.  B  /\  ( ph  /\  x  e.  A ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
109ancoms 439 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  (
y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph )
)
1110anasss 628 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
1211ancoms 439 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
13 sbceq2a 3002 . . . . . . . . . . . 12  |-  ( z  =  y  ->  ( [. z  /  y ]. ph  <->  ph ) )
1413sbcbidv 3045 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( [. w  /  x ]. [. z  /  y ]. ph  <->  [. w  /  x ]. ph ) )
1514rexbidv 2564 . . . . . . . . . 10  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. w  e.  A  [. w  /  x ]. ph )
)
1615elrab 2923 . . . . . . . . 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 203 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
)
18 sbceq2a 3002 . . . . . . . . 9  |-  ( v  =  y  ->  ( [. v  /  y ]. ph  <->  ph ) )
1918rspcev 2884 . . . . . . . 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 648 . . . . . . 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 2419 . . . . . . . 8  |-  F/_ v { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
22 nfcv 2419 . . . . . . . . . 10  |-  F/_ y A
23 nfcv 2419 . . . . . . . . . . 11  |-  F/_ y
w
24 nfsbc1v 3010 . . . . . . . . . . 11  |-  F/ y
[. z  /  y ]. ph
2523, 24nfsbc 3012 . . . . . . . . . 10  |-  F/ y
[. w  /  x ]. [. z  /  y ]. ph
2622, 25nfrex 2598 . . . . . . . . 9  |-  F/ y E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
27 nfcv 2419 . . . . . . . . 9  |-  F/_ y B
2826, 27nfrab 2721 . . . . . . . 8  |-  F/_ y { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
29 nfsbc1v 3010 . . . . . . . 8  |-  F/ y
[. v  /  y ]. ph
30 nfv 1605 . . . . . . . 8  |-  F/ v
ph
3121, 28, 29, 30, 18cbvrexf 2759 . . . . . . 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 188 . . . . . 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 587 . . . . 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 2664 . . . 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 2616 . . 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 3010 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
37 nfv 1605 . . . . . . . . 9  |-  F/ w ph
3836, 37, 6cbvrex 2761 . . . . . . . 8  |-  ( E. w  e.  A  [. w  /  x ]. ph  <->  E. x  e.  A  ph )
3915, 38syl6bb 252 . . . . . . 7  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. x  e.  A  ph ) )
4039elrab 2923 . . . . . 6  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  <->  ( y  e.  B  /\  E. x  e.  A  ph ) )
4140simprbi 450 . . . . 5  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  ->  E. x  e.  A  ph )
4241rgen 2608 . . . 4  |-  A. y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } E. x  e.  A  ph
4342a1i 10 . . 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 1132 . 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 3199 . . . . 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 2419 . . . . . . . . 9  |-  F/_ x A
47 nfsbc1v 3010 . . . . . . . . 9  |-  F/ x [. w  /  x ]. [. z  /  y ]. ph
4846, 47nfrex 2598 . . . . . . . 8  |-  F/ x E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
49 nfcv 2419 . . . . . . . 8  |-  F/_ x B
5048, 49nfrab 2721 . . . . . . 7  |-  F/_ x { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
5150nfeq2 2430 . . . . . 6  |-  F/ x  c  =  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
52 nfcv 2419 . . . . . . 7  |-  F/_ y
c
5352, 28rexeqf 2733 . . . . . 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 2561 . . . . 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 2732 . . . . 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 1252 . . . 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 2869 . . 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 418 . 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 463 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 set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934   E.wex 1528    = wceq 1623    e. wcel 1684   A.wral 2543   E.wrex 2544   {crab 2547   _Vcvv 2788   [.wsbc 2991    C_ wss 3152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator