Metamath Proof Explorer

Theorem dfwe2

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)

Ref Expression
Assertion dfwe2 
|- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )

Proof

Step Hyp Ref Expression
1 df-we 
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )
2 df-so 
 |-  ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
3 simpr 
 |-  ( ( 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 
 |-  ( x R z -> ( ( x R y /\ y R z ) -> x R z ) )
5 4 a1i 
 |-  ( ( 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 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A ) ) -> -. ( x R y /\ y R x ) )
7 6 3adantr3 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( x R y /\ y R x ) )
8 breq2 
 |-  ( x = z -> ( y R x <-> y R z ) )
9 8 anbi2d 
 |-  ( x = z -> ( ( x R y /\ y R x ) <-> ( x R y /\ y R z ) ) )
10 9 notbid 
 |-  ( x = z -> ( -. ( x R y /\ y R x ) <-> -. ( x R y /\ y R z ) ) )
11 7 10 syl5ibcom 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x = z -> -. ( x R y /\ y R z ) ) )
12 pm2.21 
 |-  ( -. ( x R y /\ y R z ) -> ( ( x R y /\ y R z ) -> x R z ) )
13 11 12 syl6 
 |-  ( ( 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 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( x R y /\ y R z /\ z R x ) )
15 df-3an 
 |-  ( ( x R y /\ y R z /\ z R x ) <-> ( ( x R y /\ y R z ) /\ z R x ) )
16 15 biimpri 
 |-  ( ( ( x R y /\ y R z ) /\ z R x ) -> ( x R y /\ y R z /\ z R x ) )
17 16 ancoms 
 |-  ( ( z R x /\ ( x R y /\ y R z ) ) -> ( x R y /\ y R z /\ z R x ) )
18 14 17 nsyl 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( z R x /\ ( x R y /\ y R z ) ) )
19 18 pm2.21d 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( z R x /\ ( x R y /\ y R z ) ) -> x R z ) )
20 19 expd 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( z R x -> ( ( x R y /\ y R z ) -> x R z ) ) )
21 5 13 20 3jaod 
 |-  ( ( 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 
 |-  ( ( R Fr A /\ x e. A ) -> -. x R x )
23 22 3ad2antr1 
 |-  ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. x R x )
24 21 23 jctild 
 |-  ( ( 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 ) ) ) )
25 24 ex 
 |-  ( 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 ) ) ) ) )
26 25 a2d 
 |-  ( 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 ) ) ) ) )
27 26 alimdv 
 |-  ( 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 ) ) ) ) )
28 27 2alimdv 
 |-  ( 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 
 |-  ( 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 
 |-  ( 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 ) ) ) )
31 28 29 30 3imtr4g 
 |-  ( 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 breq2 
 |-  ( y = z -> ( x R y <-> x R z ) )
33 equequ2 
 |-  ( y = z -> ( x = y <-> x = z ) )
34 breq1 
 |-  ( y = z -> ( y R x <-> z R x ) )
35 32 33 34 3orbi123d 
 |-  ( y = z -> ( ( x R y \/ x = y \/ y R x ) <-> ( x R z \/ x = z \/ z R x ) ) )
36 35 ralidmw 
 |-  ( 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 ) )
37 35 cbvralvw 
 |-  ( A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. z e. A ( x R z \/ x = z \/ z R x ) )
38 37 ralbii 
 |-  ( 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 ) )
39 36 38 bitr3i 
 |-  ( 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 ) )
40 39 ralbii 
 |-  ( 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 
 |-  ( 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 ) ) )
42 31 40 41 3imtr4g 
 |-  ( R Fr A -> ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> R Po A ) )
43 42 ancrd 
 |-  ( 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 ) ) ) )
44 3 43 impbid2 
 |-  ( 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 ) ) )
45 2 44 bitrid 
 |-  ( R Fr A -> ( R Or A <-> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
46 45 pm5.32i 
 |-  ( ( 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 ) ) )
47 1 46 bitri 
 |-  ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )