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

Theorem indexa 32018
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 4572 . 2  |-  ( B  e.  M  ->  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }  e.  _V )
2 ssrab2 3547 . . . 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 1752 . . . . 5  |-  F/ y  x  e.  A
5 nfre1 2887 . . . . 5  |-  F/ y E. y  e.  {
z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph } ph
6 sbceq2a 3312 . . . . . . . . . . . . . . 15  |-  ( w  =  x  ->  ( [. w  /  x ]. ph  <->  ph ) )
76rspcev 3183 . . . . . . . . . . . . . 14  |-  ( ( x  e.  A  /\  ph )  ->  E. w  e.  A  [. w  /  x ]. ph )
87ancoms 455 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  E. w  e.  A  [. w  /  x ]. ph )
98anim2i 572 . . . . . . . . . . . 12  |-  ( ( y  e.  B  /\  ( ph  /\  x  e.  A ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
109ancoms 455 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  (
y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph )
)
1110anasss 652 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
1211ancoms 455 . . . . . . . . 9  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
( y  e.  B  /\  E. w  e.  A  [. w  /  x ]. ph ) )
13 sbceq2a 3312 . . . . . . . . . . . 12  |-  ( z  =  y  ->  ( [. z  /  y ]. ph  <->  ph ) )
1413sbcbidv 3355 . . . . . . . . . . 11  |-  ( z  =  y  ->  ( [. w  /  x ]. [. z  /  y ]. ph  <->  [. w  /  x ]. ph ) )
1514rexbidv 2940 . . . . . . . . . 10  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. w  e.  A  [. w  /  x ]. ph )
)
1615elrab 3230 . . . . . . . . 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 216 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  y  e.  B
)  /\  ph )  -> 
y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
)
18 sbceq2a 3312 . . . . . . . . 9  |-  ( v  =  y  ->  ( [. v  /  y ]. ph  <->  ph ) )
1918rspcev 3183 . . . . . . . 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 672 . . . . . . 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 2585 . . . . . . . 8  |-  F/_ v { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
22 nfcv 2585 . . . . . . . . . 10  |-  F/_ y A
23 nfcv 2585 . . . . . . . . . . 11  |-  F/_ y
w
24 nfsbc1v 3320 . . . . . . . . . . 11  |-  F/ y
[. z  /  y ]. ph
2523, 24nfsbc 3322 . . . . . . . . . 10  |-  F/ y
[. w  /  x ]. [. z  /  y ]. ph
2622, 25nfrex 2889 . . . . . . . . 9  |-  F/ y E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
27 nfcv 2585 . . . . . . . . 9  |-  F/_ y B
2826, 27nfrab 3011 . . . . . . . 8  |-  F/_ y { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
29 nfsbc1v 3320 . . . . . . . 8  |-  F/ y
[. v  /  y ]. ph
30 nfv 1752 . . . . . . . 8  |-  F/ v
ph
3121, 28, 29, 30, 18cbvrexf 3051 . . . . . . 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 200 . . . . . 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 608 . . . . 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 2910 . . . 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 2817 . . 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 3320 . . . . . . . . 9  |-  F/ x [. w  /  x ]. ph
37 nfv 1752 . . . . . . . . 9  |-  F/ w ph
3836, 37, 6cbvrex 3053 . . . . . . . 8  |-  ( E. w  e.  A  [. w  /  x ]. ph  <->  E. x  e.  A  ph )
3915, 38syl6bb 265 . . . . . . 7  |-  ( z  =  y  ->  ( E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph  <->  E. x  e.  A  ph ) )
4039elrab 3230 . . . . . 6  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  <->  ( y  e.  B  /\  E. x  e.  A  ph ) )
4140simprbi 466 . . . . 5  |-  ( y  e.  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  / 
y ]. ph }  ->  E. x  e.  A  ph )
4241rgen 2786 . . . 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 1186 . 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 3486 . . . . 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 2585 . . . . . . . . 9  |-  F/_ x A
47 nfsbc1v 3320 . . . . . . . . 9  |-  F/ x [. w  /  x ]. [. z  /  y ]. ph
4846, 47nfrex 2889 . . . . . . . 8  |-  F/ x E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph
49 nfcv 2585 . . . . . . . 8  |-  F/_ x B
5048, 49nfrab 3011 . . . . . . 7  |-  F/_ x { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
5150nfeq2 2602 . . . . . 6  |-  F/ x  c  =  { z  e.  B  |  E. w  e.  A  [. w  /  x ]. [. z  /  y ]. ph }
52 nfcv 2585 . . . . . . 7  |-  F/_ y
c
5352, 28rexeqf 3023 . . . . . 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 2860 . . . . 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 3022 . . . . 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 1336 . . . 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 3168 . . 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 431 . 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 480 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 371    /\ w3a 983    = wceq 1438   E.wex 1660    e. wcel 1869   A.wral 2776   E.wrex 2777   {crab 2780   _Vcvv 3082   [.wsbc 3300    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-in 3444  df-ss 3451
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator