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

Theorem ac10ct 8305
Description: A proof of the Well ordering theorem weth 8765, 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 3071 . . . . . 6  |-  y  e. 
_V
21brdom 7422 . . . . 5  |-  ( A  ~<_  y  <->  E. f  f : A -1-1-> y )
3 f1f 5704 . . . . . . . . . . . 12  |-  ( f : A -1-1-> y  -> 
f : A --> y )
4 frn 5663 . . . . . . . . . . . 12  |-  ( f : A --> y  ->  ran  f  C_  y )
53, 4syl 16 . . . . . . . . . . 11  |-  ( f : A -1-1-> y  ->  ran  f  C_  y )
6 onss 6502 . . . . . . . . . . 11  |-  ( y  e.  On  ->  y  C_  On )
7 sstr2 3461 . . . . . . . . . . 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 6495 . . . . . . . . . 10  |-  _E  We  On
10 wess 4805 . . . . . . . . . 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 5750 . . . . . . . . . 10  |-  ( f : A -1-1-> y  -> 
f : A -1-1-onto-> ran  f
)
14 eqid 2451 . . . . . . . . . . 11  |-  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) }  =  { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }
1514f1owe 6143 . . . . . . . . . 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 5004 . . . . . . . . . 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 7416 . . . . . . . . . . . 12  |-  Rel  ~<_
1918brrelexi 4977 . . . . . . . . . . 11  |-  ( A  ~<_  y  ->  A  e.  _V )
20 xpexg 6607 . . . . . . . . . . . 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 3641 . . . . . . . . . . . 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 4533 . . . . . . . . . . . 12  |-  ( ( A  X.  A )  e.  _V  ->  (
( A  X.  A
)  i^i  { <. w ,  z >.  |  ( f `  w )  _E  ( f `  z ) } )  e.  _V )
2422, 23syl5eqelr 2544 . . . . . . . . . . 11  |-  ( ( A  X.  A )  e.  _V  ->  ( { <. w ,  z
>.  |  ( f `  w )  _E  (
f `  z ) }  i^i  ( A  X.  A ) )  e. 
_V )
25 weeq1 4806 . . . . . . . . . . . 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 3154 . . . . . . . . . . 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 1691 . . . . 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 2931 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 1587    e. wcel 1758   E.wrex 2796   _Vcvv 3068    i^i cin 3425    C_ wss 3426   class class class wbr 4390   {copab 4447    _E cep 4728    We wwe 4776   Oncon0 4817    X. cxp 4936   ran crn 4939   -->wf 5512   -1-1->wf1 5513   -1-1-onto->wf1o 5515   ` cfv 5516    ~<_ cdom 7408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-rep 4501  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-pss 3442  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-tp 3980  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-tr 4484  df-eprel 4730  df-id 4734  df-po 4739  df-so 4740  df-fr 4777  df-we 4779  df-ord 4820  df-on 4821  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-isom 5525  df-dom 7412
This theorem is referenced by:  ondomen  8308
  Copyright terms: Public domain W3C validator