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

Theorem dfwe2 4765
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
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-we 4546 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
2 df-so 4507 . . . 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 6 . . . . . . . . . . . . . . 15  |-  ( x R z  ->  (
( x R y  /\  y R z )  ->  x R
z ) )
54a1i 11 . . . . . . . . . . . . . 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 4563 . . . . . . . . . . . . . . . . 17  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A
) )  ->  -.  ( x R y  /\  y R x ) )
763adantr3 1119 . . . . . . . . . . . . . . . 16  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  ( x R y  /\  y R x ) )
8 breq2 4219 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  z  ->  (
y R x  <->  y R
z ) )
98anbi2d 686 . . . . . . . . . . . . . . . . 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 103 . . . . . . . . . . . . . . 15  |-  ( -.  ( x R y  /\  y R z )  ->  ( (
x R y  /\  y R z )  ->  x R z ) )
1311, 12syl6 32 . . . . . . . . . . . . . 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 4763 . . . . . . . . . . . . . . . . 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 939 . . . . . . . . . . . . . . . . . . 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 116 . . . . . . . . . . . . . . . 16  |-  ( ( R  Fr  A  /\  ( x  e.  A  /\  y  e.  A  /\  z  e.  A
) )  ->  -.  ( z R x  /\  ( x R y  /\  y R z ) ) )
1918pm2.21d 101 . . . . . . . . . . . . . . 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 1249 . . . . . . . . . . . . 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 4562 . . . . . . . . . . . . . 14  |-  ( ( R  Fr  A  /\  x  e.  A )  ->  -.  x R x )
23223ad2antr1 1123 . . . . . . . . . . . . 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 1632 . . . . . . . . 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 1634 . . . . . . . 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 2765 . . . . . . . 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 2765 . . . . . . . 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 3733 . . . . . . . . 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 4219 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
x R y  <->  x R
z ) )
34 equequ2 1699 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
x  =  y  <->  x  =  z ) )
35 breq1 4218 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y R x  <->  z R x ) )
3633, 34, 353orbi123d 1254 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( x R y  \/  x  =  y  \/  y R x )  <->  ( x R z  \/  x  =  z  \/  z R x ) ) )
3736cbvralv 2934 . . . . . . . . . 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 2731 . . . . . . . . 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 2731 . . . . . . 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 4506 . . . . . . 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 620 . 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 3    -> wi 4    <-> wb 178    /\ wa 360    \/ w3o 936    /\ w3a 937   A.wal 1550    e. wcel 1726   A.wral 2707   class class class wbr 4215    Po wpo 4504    Or wor 4505    Fr wfr 4541    We wwe 4543
This theorem is referenced by:  ordon  4766  f1oweALT  6077  dford2  7578  fpwwe2lem12  8521  fpwwe2lem13  8522  dfon2  25424  fnwe2  27142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pr 4406  ax-un 4704
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-br 4216  df-po 4506  df-so 4507  df-fr 4544  df-we 4546
  Copyright terms: Public domain W3C validator