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

Theorem dfwe2 4510
Description: Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)
Assertion
Ref Expression
dfwe2  |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
Distinct variable groups:    x, y, R    x, A, y

Proof of Theorem dfwe2
StepHypRef Expression
1 df-we 4291 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
2 df-so 4252 . . . 4  |-  ( R  Or  A  <->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
3 simpr 449 . . . . 5  |-  ( ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) )  ->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )
4 ax-1 7 . . . . . . . . . . . . . . 15  |-  ( x R z  ->  (
( x R y  /\  y R z )  ->  x R
z ) )
54a1i 12 . . . . . . . . . . . . . 14  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
x R z  -> 
( ( x R y  /\  y R z )  ->  x R z ) ) )
6 fr2nr 4308 . . . . . . . . . . . . . . . . 17  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A
) )  ->  -.  ( x R y  /\  y R x ) )
763adantr3 1121 . . . . . . . . . . . . . . . 16  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  ( x R y  /\  y R x ) )
8 breq2 3967 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
y R x  <->  y R
z ) )
98anbi2d 687 . . . . . . . . . . . . . . . . 17  |-  ( x  =  z  ->  (
( x R y  /\  y R x )  <->  ( x R y  /\  y R z ) ) )
109notbid 287 . . . . . . . . . . . . . . . 16  |-  ( x  =  z  ->  ( -.  ( x R y  /\  y R x )  <->  -.  ( x R y  /\  y R z ) ) )
117, 10syl5ibcom 213 . . . . . . . . . . . . . . 15  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
x  =  z  ->  -.  ( x R y  /\  y R z ) ) )
12 pm2.21 102 . . . . . . . . . . . . . . 15  |-  ( -.  ( x R y  /\  y R z )  ->  ( (
x R y  /\  y R z )  ->  x R z ) )
1311, 12syl6 31 . . . . . . . . . . . . . 14  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
x  =  z  -> 
( ( x R y  /\  y R z )  ->  x R z ) ) )
14 fr3nr 4508 . . . . . . . . . . . . . . . . 17  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  ( x R y  /\  y R z  /\  z R x ) )
15 df-3an 941 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x R y  /\  y R z  /\  z R x )  <->  ( (
x R y  /\  y R z )  /\  z R x ) )
1615biimpri 199 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( x R y  /\  y R z )  /\  z R x )  ->  (
x R y  /\  y R z  /\  z R x ) )
1716ancoms 441 . . . . . . . . . . . . . . . . 17  |-  ( ( z R x  /\  ( x R y  /\  y R z ) )  ->  (
x R y  /\  y R z  /\  z R x ) )
1814, 17nsyl 115 . . . . . . . . . . . . . . . 16  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  ( z R x  /\  ( x R y  /\  y R z ) ) )
1918pm2.21d 100 . . . . . . . . . . . . . . 15  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
( z R x  /\  ( x R y  /\  y R z ) )  ->  x R z ) )
2019exp3a 427 . . . . . . . . . . . . . 14  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
z R x  -> 
( ( x R y  /\  y R z )  ->  x R z ) ) )
215, 13, 203jaod 1251 . . . . . . . . . . . . 13  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
( x R z  \/  x  =  z  \/  z R x )  ->  ( (
x R y  /\  y R z )  ->  x R z ) ) )
22 frirr 4307 . . . . . . . . . . . . . 14  |-  ( ( R  Fr  A  /\  x  e.  A )  ->  -.  x R x )
23223ad2antr1 1125 . . . . . . . . . . . . 13  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  x R x )
2421, 23jctild 529 . . . . . . . . . . . 12  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  (
( x R z  \/  x  =  z  \/  z R x )  ->  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) ) )
2524ex 425 . . . . . . . . . . 11  |-  ( R  Fr  A  ->  (
( x  e.  A  /\  y  e.  A  /\  z  e.  A
)  ->  ( (
x R z  \/  x  =  z  \/  z R x )  ->  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) ) ) )
2625a2d 25 . . . . . . . . . 10  |-  ( R  Fr  A  ->  (
( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  (
x R z  \/  x  =  z  \/  z R x ) )  ->  ( (
x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) ) ) )
2726alimdv 2018 . . . . . . . . 9  |-  ( R  Fr  A  ->  ( A. z ( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  (
x R z  \/  x  =  z  \/  z R x ) )  ->  A. z
( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) ) ) )
28272alimdv 2020 . . . . . . . 8  |-  ( R  Fr  A  ->  ( A. x A. y A. z ( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  (
x R z  \/  x  =  z  \/  z R x ) )  ->  A. x A. y A. z ( ( x  e.  A  /\  y  e.  A  /\  z  e.  A
)  ->  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) ) ) )
29 r3al 2571 . . . . . . . 8  |-  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  (
x R z  \/  x  =  z  \/  z R x )  <->  A. x A. y A. z ( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  (
x R z  \/  x  =  z  \/  z R x ) ) )
30 r3al 2571 . . . . . . . 8  |-  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) )  <->  A. x A. y A. z ( ( x  e.  A  /\  y  e.  A  /\  z  e.  A )  ->  ( -.  x R x  /\  ( ( x R y  /\  y R z )  ->  x R z ) ) ) )
3128, 29, 303imtr4g 263 . . . . . . 7  |-  ( R  Fr  A  ->  ( A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R z  \/  x  =  z  \/  z R x )  ->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) ) )
32 ralidm 3499 . . . . . . . . 9  |-  ( A. y  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )
33 breq2 3967 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
x R y  <->  x R
z ) )
34 equequ2 1830 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
x  =  y  <->  x  =  z ) )
35 breq1 3966 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y R x  <->  z R x ) )
3633, 34, 353orbi123d 1256 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( x R y  \/  x  =  y  \/  y R x )  <->  ( x R z  \/  x  =  z  \/  z R x ) ) )
3736cbvralv 2717 . . . . . . . . . 10  |-  ( A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. z  e.  A  ( x R z  \/  x  =  z  \/  z R x ) )
3837ralbii 2538 . . . . . . . . 9  |-  ( A. y  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. y  e.  A  A. z  e.  A  ( x R z  \/  x  =  z  \/  z R x ) )
3932, 38bitr3i 244 . . . . . . . 8  |-  ( A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. y  e.  A  A. z  e.  A  ( x R z  \/  x  =  z  \/  z R x ) )
4039ralbii 2538 . . . . . . 7  |-  ( A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x )  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( x R z  \/  x  =  z  \/  z R x ) )
41 df-po 4251 . . . . . . 7  |-  ( R  Po  A  <->  A. x  e.  A  A. y  e.  A  A. z  e.  A  ( -.  x R x  /\  (
( x R y  /\  y R z )  ->  x R
z ) ) )
4231, 40, 413imtr4g 263 . . . . . 6  |-  ( R  Fr  A  ->  ( A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )  ->  R  Po  A ) )
4342ancrd 539 . . . . 5  |-  ( R  Fr  A  ->  ( A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x )  ->  ( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) ) )
443, 43impbid2 197 . . . 4  |-  ( R  Fr  A  ->  (
( R  Po  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) )  <->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
452, 44syl5bb 250 . . 3  |-  ( R  Fr  A  ->  ( R  Or  A  <->  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
4645pm5.32i 621 . 2  |-  ( ( R  Fr  A  /\  R  Or  A )  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  (
x R y  \/  x  =  y  \/  y R x ) ) )
471, 46bitri 242 1  |-  ( R  We  A  <->  ( R  Fr  A  /\  A. x  e.  A  A. y  e.  A  ( x R y  \/  x  =  y  \/  y R x ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    <-> wb 178    /\ wa 360    \/ w3o 938    /\ w3a 939   A.wal 1532    = wceq 1619    e. wcel 1621   A.wral 2516   class class class wbr 3963    Po wpo 4249    Or wor 4250    Fr wfr 4286    We wwe 4288
This theorem is referenced by:  ordon  4511  f1oweALT  5750  dford2  7254  fpwwe2lem12  8196  fpwwe2lem13  8197  dfon2  23482  fnwe2  26482
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-rab 2523  df-v 2742  df-sbc 2936  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-br 3964  df-po 4251  df-so 4252  df-fr 4289  df-we 4291
  Copyright terms: Public domain W3C validator