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

Theorem indexa 26449
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 4356 . 2  |-  ( B  e.  M  ->  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  e.  _V )
2 ssrab2 3430 . . . 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 1630 . . . . 5  |-  F/ y  x  e.  A
5 nfre1 2764 . . . . 5  |-  F/ y E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph
6 sbceq2a 3174 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( [. w  /  x ]. ph  <->  ph ) )
76rspcev 3054 . . . . . . . . . . . . . 14  |-  ( ( x  e.  A  /\  ph )  ->  E. w  e.  A  [. w  /  x ]. ph )
87ancoms 441 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  E. w  e.  A  [. w  /  x ]. ph )
98anim2i 554 . . . . . . . . . . . 12  |-  ( ( y  e.  B  /\  ( ph  /\  x  e.  A ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
109ancoms 441 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  (
y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph )
)
1110anasss 630 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
1211ancoms 441 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
13 sbceq2a 3174 . . . . . . . . . . . 12  |-  ( z  =  y  ->  ( [. z  /  y ]. ph  <->  ph ) )
1413sbcbidv 3217 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( [. w  /  x ]. [. z  /  y ]. ph  <->  [. w  /  x ]. ph ) )
1514rexbidv 2728 . . . . . . . . . 10  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. w  e.  A  [. w  /  x ]. ph )
)
1615elrab 3094 . . . . . . . . 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 205 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
)
18 sbceq2a 3174 . . . . . . . . 9  |-  ( v  =  y  ->  ( [. v  /  y ]. ph  <->  ph ) )
1918rspcev 3054 . . . . . . . 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 650 . . . . . . 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 2574 . . . . . . . 8  |-  F/_ v { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
22 nfcv 2574 . . . . . . . . . 10  |-  F/_ y A
23 nfcv 2574 . . . . . . . . . . 11  |-  F/_ y
w
24 nfsbc1v 3182 . . . . . . . . . . 11  |-  F/ y
[. z  /  y ]. ph
2523, 24nfsbc 3184 . . . . . . . . . 10  |-  F/ y
[. w  /  x ]. [. z  /  y ]. ph
2622, 25nfrex 2763 . . . . . . . . 9  |-  F/ y E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
27 nfcv 2574 . . . . . . . . 9  |-  F/_ y B
2826, 27nfrab 2891 . . . . . . . 8  |-  F/_ y { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
29 nfsbc1v 3182 . . . . . . . 8  |-  F/ y
[. v  /  y ]. ph
30 nfv 1630 . . . . . . . 8  |-  F/ v
ph
3121, 28, 29, 30, 18cbvrexf 2929 . . . . . . 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 190 . . . . . 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 589 . . . . 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 2829 . . . 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 2781 . . 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 3182 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
37 nfv 1630 . . . . . . . . 9  |-  F/ w ph
3836, 37, 6cbvrex 2931 . . . . . . . 8  |-  ( E. w  e.  A  [. w  /  x ]. ph  <->  E. x  e.  A  ph )
3915, 38syl6bb 254 . . . . . . 7  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. x  e.  A  ph ) )
4039elrab 3094 . . . . . 6  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  <->  ( y  e.  B  /\  E. x  e.  A  ph ) )
4140simprbi 452 . . . . 5  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  ->  E. x  e.  A  ph )
4241rgen 2773 . . . 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 1135 . 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 3371 . . . . 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 2574 . . . . . . . . 9  |-  F/_ x A
47 nfsbc1v 3182 . . . . . . . . 9  |-  F/ x [. w  /  x ]. [. z  /  y ]. ph
4846, 47nfrex 2763 . . . . . . . 8  |-  F/ x E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
49 nfcv 2574 . . . . . . . 8  |-  F/_ x B
5048, 49nfrab 2891 . . . . . . 7  |-  F/_ x { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
5150nfeq2 2585 . . . . . 6  |-  F/ x  c  =  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
52 nfcv 2574 . . . . . . 7  |-  F/_ y
c
5352, 28rexeqf 2903 . . . . . 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 2725 . . . . 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 2902 . . . . 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 1255 . . . 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 3039 . . 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 420 . 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 465 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 360    /\ w3a 937   E.wex 1551    = wceq 1653    e. wcel 1726   A.wral 2707   E.wrex 2708   {crab 2711   _Vcvv 2958   [.wsbc 3163    C_ wss 3322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator