MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ac10ct Structured version   Unicode version

Theorem ac10ct 8196
Description: A proof of the Well ordering theorem weth 8656, an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013.)
Assertion
Ref Expression
ac10ct  |-  ( E. y  e.  On  A  ~<_  y  ->  E. x  x  We  A )
Distinct variable group:    x, A, y

Proof of Theorem ac10ct
Dummy variables  f  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2969 . . . . . 6  |-  y  e. 
_V
21brdom 7314 . . . . 5  |-  ( A  ~<_  y  <->  E. f  f : A -1-1-> y )
3 f1f 5599 . . . . . . . . . . . 12  |-  ( f : A -1-1-> y  -> 
f : A --> y )
4 frn 5558 . . . . . . . . . . . 12  |-  ( f : A --> y  ->  ran  f  C_  y )
53, 4syl 16 . . . . . . . . . . 11  |-  ( f : A -1-1-> y  ->  ran  f  C_  y )
6 onss 6397 . . . . . . . . . . 11  |-  ( y  e.  On  ->  y  C_  On )
7 sstr2 3356 . . . . . . . . . . 11  |-  ( ran  f  C_  y  ->  ( y  C_  On  ->  ran  f  C_  On )
)
85, 6, 7syl2im 38 . . . . . . . . . 10  |-  ( f : A -1-1-> y  -> 
( y  e.  On  ->  ran  f  C_  On ) )
9 epweon 6390 . . . . . . . . . 10  |-  _E  We  On
10 wess 4699 . . . . . . . . . 10  |-  ( ran  f  C_  On  ->  (  _E  We  On  ->  _E  We  ran  f ) )
118, 9, 10syl6mpi 62 . . . . . . . . 9  |-  ( f : A -1-1-> y  -> 
( y  e.  On  ->  _E  We  ran  f
) )
1211adantl 466 . . . . . . . 8  |-  ( ( A  ~<_  y  /\  f : A -1-1-> y )  -> 
( y  e.  On  ->  _E  We  ran  f
) )
13 f1f1orn 5645 . . . . . . . . . 10  |-  ( f : A -1-1-> y  -> 
f : A -1-1-onto-> ran  f
)
14 eqid 2437 . . . . . . . . . . 11  |-  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) }  =  { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }
1514f1owe 6037 . . . . . . . . . 10  |-  ( f : A -1-1-onto-> ran  f  ->  (  _E  We  ran  f  ->  { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }  We  A )
)
1613, 15syl 16 . . . . . . . . 9  |-  ( f : A -1-1-> y  -> 
(  _E  We  ran  f  ->  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) }  We  A ) )
17 weinxp 4898 . . . . . . . . . 10  |-  ( {
<. w ,  z >.  |  ( f `  w )  _E  (
f `  z ) }  We  A  <->  ( { <. w ,  z >.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  We  A )
18 reldom 7308 . . . . . . . . . . . 12  |-  Rel  ~<_
1918brrelexi 4871 . . . . . . . . . . 11  |-  ( A  ~<_  y  ->  A  e.  _V )
20 xpexg 6502 . . . . . . . . . . . 12  |-  ( ( A  e.  _V  /\  A  e.  _V )  ->  ( A  X.  A
)  e.  _V )
2120anidms 645 . . . . . . . . . . 11  |-  ( A  e.  _V  ->  ( A  X.  A )  e. 
_V )
22 incom 3536 . . . . . . . . . . . 12  |-  ( ( A  X.  A )  i^i  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) } )  =  ( { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) }  i^i  ( A  X.  A
) )
23 inex1g 4428 . . . . . . . . . . . 12  |-  ( ( A  X.  A )  e.  _V  ->  (
( A  X.  A
)  i^i  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) } )  e.  _V )
2422, 23syl5eqelr 2522 . . . . . . . . . . 11  |-  ( ( A  X.  A )  e.  _V  ->  ( { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  e. 
_V )
25 weeq1 4700 . . . . . . . . . . . 12  |-  ( x  =  ( { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) }  i^i  ( A  X.  A
) )  ->  (
x  We  A  <->  ( { <. w ,  z >.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  We  A ) )
2625spcegv 3051 . . . . . . . . . . 11  |-  ( ( { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  e. 
_V  ->  ( ( {
<. w ,  z >.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  We  A  ->  E. x  x  We  A )
)
2719, 21, 24, 264syl 21 . . . . . . . . . 10  |-  ( A  ~<_  y  ->  ( ( { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  We  A  ->  E. x  x  We  A )
)
2817, 27syl5bi 217 . . . . . . . . 9  |-  ( A  ~<_  y  ->  ( { <. w ,  z >.  |  ( f `  w )  _E  (
f `  z ) }  We  A  ->  E. x  x  We  A
) )
2916, 28sylan9r 658 . . . . . . . 8  |-  ( ( A  ~<_  y  /\  f : A -1-1-> y )  -> 
(  _E  We  ran  f  ->  E. x  x  We  A ) )
3012, 29syld 44 . . . . . . 7  |-  ( ( A  ~<_  y  /\  f : A -1-1-> y )  -> 
( y  e.  On  ->  E. x  x  We  A ) )
3130impancom 440 . . . . . 6  |-  ( ( A  ~<_  y  /\  y  e.  On )  ->  (
f : A -1-1-> y  ->  E. x  x  We  A ) )
3231exlimdv 1690 . . . . 5  |-  ( ( A  ~<_  y  /\  y  e.  On )  ->  ( E. f  f : A -1-1-> y  ->  E. x  x  We  A )
)
332, 32syl5bi 217 . . . 4  |-  ( ( A  ~<_  y  /\  y  e.  On )  ->  ( A  ~<_  y  ->  E. x  x  We  A )
)
3433ex 434 . . 3  |-  ( A  ~<_  y  ->  ( y  e.  On  ->  ( A  ~<_  y  ->  E. x  x  We  A ) ) )
3534pm2.43b 50 . 2  |-  ( y  e.  On  ->  ( A  ~<_  y  ->  E. x  x  We  A )
)
3635rexlimiv 2829 1  |-  ( E. y  e.  On  A  ~<_  y  ->  E. x  x  We  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586    e. wcel 1756   E.wrex 2710   _Vcvv 2966    i^i cin 3320    C_ wss 3321   class class class wbr 4285   {copab 4342    _E cep 4622    We wwe 4670   Oncon0 4711    X. cxp 4830   ran crn 4833   -->wf 5407   -1-1->wf1 5408   -1-1-onto->wf1o 5410   ` cfv 5411    ~<_ cdom 7300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-tp 3875  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-tr 4379  df-eprel 4624  df-id 4628  df-po 4633  df-so 4634  df-fr 4671  df-we 4673  df-ord 4714  df-on 4715  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-isom 5420  df-dom 7304
This theorem is referenced by:  ondomen  8199
  Copyright terms: Public domain W3C validator