Metamath Proof Explorer


Theorem fr3nr

Description: A well-founded relation has no 3-cycle loops. Special case of Proposition 6.23 of TakeutiZaring p. 30. (Contributed by NM, 10-Apr-1994) (Revised by Mario Carneiro, 22-Jun-2015)

Ref Expression
Assertion fr3nr R Fr A B A C A D A ¬ B R C C R D D R B

Proof

Step Hyp Ref Expression
1 tpex B C D V
2 1 a1i R Fr A B A C A D A B C D V
3 simpl R Fr A B A C A D A R Fr A
4 df-tp B C D = B C D
5 simpr1 R Fr A B A C A D A B A
6 simpr2 R Fr A B A C A D A C A
7 5 6 prssd R Fr A B A C A D A B C A
8 simpr3 R Fr A B A C A D A D A
9 8 snssd R Fr A B A C A D A D A
10 7 9 unssd R Fr A B A C A D A B C D A
11 4 10 eqsstrid R Fr A B A C A D A B C D A
12 5 tpnzd R Fr A B A C A D A B C D
13 fri B C D V R Fr A B C D A B C D x B C D y B C D ¬ y R x
14 2 3 11 12 13 syl22anc R Fr A B A C A D A x B C D y B C D ¬ y R x
15 breq2 x = B y R x y R B
16 15 notbid x = B ¬ y R x ¬ y R B
17 16 ralbidv x = B y B C D ¬ y R x y B C D ¬ y R B
18 breq2 x = C y R x y R C
19 18 notbid x = C ¬ y R x ¬ y R C
20 19 ralbidv x = C y B C D ¬ y R x y B C D ¬ y R C
21 breq2 x = D y R x y R D
22 21 notbid x = D ¬ y R x ¬ y R D
23 22 ralbidv x = D y B C D ¬ y R x y B C D ¬ y R D
24 17 20 23 rextpg B A C A D A x B C D y B C D ¬ y R x y B C D ¬ y R B y B C D ¬ y R C y B C D ¬ y R D
25 24 adantl R Fr A B A C A D A x B C D y B C D ¬ y R x y B C D ¬ y R B y B C D ¬ y R C y B C D ¬ y R D
26 14 25 mpbid R Fr A B A C A D A y B C D ¬ y R B y B C D ¬ y R C y B C D ¬ y R D
27 snsstp3 D B C D
28 snssg D A D B C D D B C D
29 8 28 syl R Fr A B A C A D A D B C D D B C D
30 27 29 mpbiri R Fr A B A C A D A D B C D
31 breq1 y = D y R B D R B
32 31 notbid y = D ¬ y R B ¬ D R B
33 32 rspcv D B C D y B C D ¬ y R B ¬ D R B
34 30 33 syl R Fr A B A C A D A y B C D ¬ y R B ¬ D R B
35 snsstp1 B B C D
36 snssg B A B B C D B B C D
37 5 36 syl R Fr A B A C A D A B B C D B B C D
38 35 37 mpbiri R Fr A B A C A D A B B C D
39 breq1 y = B y R C B R C
40 39 notbid y = B ¬ y R C ¬ B R C
41 40 rspcv B B C D y B C D ¬ y R C ¬ B R C
42 38 41 syl R Fr A B A C A D A y B C D ¬ y R C ¬ B R C
43 snsstp2 C B C D
44 snssg C A C B C D C B C D
45 6 44 syl R Fr A B A C A D A C B C D C B C D
46 43 45 mpbiri R Fr A B A C A D A C B C D
47 breq1 y = C y R D C R D
48 47 notbid y = C ¬ y R D ¬ C R D
49 48 rspcv C B C D y B C D ¬ y R D ¬ C R D
50 46 49 syl R Fr A B A C A D A y B C D ¬ y R D ¬ C R D
51 34 42 50 3orim123d R Fr A B A C A D A y B C D ¬ y R B y B C D ¬ y R C y B C D ¬ y R D ¬ D R B ¬ B R C ¬ C R D
52 26 51 mpd R Fr A B A C A D A ¬ D R B ¬ B R C ¬ C R D
53 3ianor ¬ D R B B R C C R D ¬ D R B ¬ B R C ¬ C R D
54 52 53 sylibr R Fr A B A C A D A ¬ D R B B R C C R D
55 3anrot D R B B R C C R D B R C C R D D R B
56 54 55 sylnib R Fr A B A C A D A ¬ B R C C R D D R B