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

Theorem indexa 29678
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 4590 . 2  |-  ( B  e.  M  ->  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  e.  _V )
2 ssrab2 3578 . . . 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 1678 . . . . 5  |-  F/ y  x  e.  A
5 nfre1 2918 . . . . 5  |-  F/ y E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph
6 sbceq2a 3336 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( [. w  /  x ]. ph  <->  ph ) )
76rspcev 3207 . . . . . . . . . . . . . 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 3336 . . . . . . . . . . . 12  |-  ( z  =  y  ->  ( [. z  /  y ]. ph  <->  ph ) )
1413sbcbidv 3383 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( [. w  /  x ]. [. z  /  y ]. ph  <->  [. w  /  x ]. ph ) )
1514rexbidv 2966 . . . . . . . . . 10  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. w  e.  A  [. w  /  x ]. ph )
)
1615elrab 3254 . . . . . . . . 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 3336 . . . . . . . . 9  |-  ( v  =  y  ->  ( [. v  /  y ]. ph  <->  ph ) )
1918rspcev 3207 . . . . . . . 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 2622 . . . . . . . 8  |-  F/_ v { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
22 nfcv 2622 . . . . . . . . . 10  |-  F/_ y A
23 nfcv 2622 . . . . . . . . . . 11  |-  F/_ y
w
24 nfsbc1v 3344 . . . . . . . . . . 11  |-  F/ y
[. z  /  y ]. ph
2523, 24nfsbc 3346 . . . . . . . . . 10  |-  F/ y
[. w  /  x ]. [. z  /  y ]. ph
2622, 25nfrex 2920 . . . . . . . . 9  |-  F/ y E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
27 nfcv 2622 . . . . . . . . 9  |-  F/_ y B
2826, 27nfrab 3036 . . . . . . . 8  |-  F/_ y { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
29 nfsbc1v 3344 . . . . . . . 8  |-  F/ y
[. v  /  y ]. ph
30 nfv 1678 . . . . . . . 8  |-  F/ v
ph
3121, 28, 29, 30, 18cbvrexf 3076 . . . . . . 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 2940 . . . 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 2848 . . 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 3344 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
37 nfv 1678 . . . . . . . . 9  |-  F/ w ph
3836, 37, 6cbvrex 3078 . . . . . . . 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 3254 . . . . . 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 2817 . . . 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 1171 . 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 3518 . . . . 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 2622 . . . . . . . . 9  |-  F/_ x A
47 nfsbc1v 3344 . . . . . . . . 9  |-  F/ x [. w  /  x ]. [. z  /  y ]. ph
4846, 47nfrex 2920 . . . . . . . 8  |-  F/ x E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
49 nfcv 2622 . . . . . . . 8  |-  F/_ x B
5048, 49nfrab 3036 . . . . . . 7  |-  F/_ x { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
5150nfeq2 2639 . . . . . 6  |-  F/ x  c  =  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
52 nfcv 2622 . . . . . . 7  |-  F/_ y
c
5352, 28rexeqf 3048 . . . . . 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 2891 . . . . 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 3047 . . . . 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 1294 . . . 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 3192 . . 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 968    = wceq 1374   E.wex 1591    e. wcel 1762   A.wral 2807   E.wrex 2808   {crab 2811   _Vcvv 3106   [.wsbc 3324    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-in 3476  df-ss 3483
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator