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
|
syl5bb |
|- ( 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 ) ) ) |