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 e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )

Proof

Step Hyp Ref Expression
1 tpex
 |-  { B , C , D } e. _V
2 1 a1i
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } e. _V )
3 simpl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> R Fr A )
4 df-tp
 |-  { B , C , D } = ( { B , C } u. { D } )
5 simpr1
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> B e. A )
6 simpr2
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> C e. A )
7 5 6 prssd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C } C_ A )
8 simpr3
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> D e. A )
9 8 snssd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { D } C_ A )
10 7 9 unssd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( { B , C } u. { D } ) C_ A )
11 4 10 eqsstrid
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } C_ A )
12 5 tpnzd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> { B , C , D } =/= (/) )
13 fri
 |-  ( ( ( { B , C , D } e. _V /\ R Fr A ) /\ ( { B , C , D } C_ A /\ { B , C , D } =/= (/) ) ) -> E. x e. { B , C , D } A. y e. { B , C , D } -. y R x )
14 2 3 11 12 13 syl22anc
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> E. x e. { B , C , D } A. y e. { 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 -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { 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 -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { 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 -> ( A. y e. { B , C , D } -. y R x <-> A. y e. { B , C , D } -. y R D ) )
24 17 20 23 rextpg
 |-  ( ( B e. A /\ C e. A /\ D e. A ) -> ( E. x e. { B , C , D } A. y e. { B , C , D } -. y R x <-> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) ) )
25 24 adantl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( E. x e. { B , C , D } A. y e. { B , C , D } -. y R x <-> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) ) )
26 14 25 mpbid
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) )
27 snsstp3
 |-  { D } C_ { B , C , D }
28 snssg
 |-  ( D e. A -> ( D e. { B , C , D } <-> { D } C_ { B , C , D } ) )
29 8 28 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( D e. { B , C , D } <-> { D } C_ { B , C , D } ) )
30 27 29 mpbiri
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> D e. { 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 e. { B , C , D } -> ( A. y e. { B , C , D } -. y R B -> -. D R B ) )
34 30 33 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R B -> -. D R B ) )
35 snsstp1
 |-  { B } C_ { B , C , D }
36 snssg
 |-  ( B e. A -> ( B e. { B , C , D } <-> { B } C_ { B , C , D } ) )
37 5 36 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( B e. { B , C , D } <-> { B } C_ { B , C , D } ) )
38 35 37 mpbiri
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> B e. { 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 e. { B , C , D } -> ( A. y e. { B , C , D } -. y R C -> -. B R C ) )
42 38 41 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R C -> -. B R C ) )
43 snsstp2
 |-  { C } C_ { B , C , D }
44 snssg
 |-  ( C e. A -> ( C e. { B , C , D } <-> { C } C_ { B , C , D } ) )
45 6 44 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( C e. { B , C , D } <-> { C } C_ { B , C , D } ) )
46 43 45 mpbiri
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> C e. { 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 e. { B , C , D } -> ( A. y e. { B , C , D } -. y R D -> -. C R D ) )
50 46 49 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( A. y e. { B , C , D } -. y R D -> -. C R D ) )
51 34 42 50 3orim123d
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. A ) ) -> ( ( A. y e. { B , C , D } -. y R B \/ A. y e. { B , C , D } -. y R C \/ A. y e. { B , C , D } -. y R D ) -> ( -. D R B \/ -. B R C \/ -. C R D ) ) )
52 26 51 mpd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A /\ D e. 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 e. A /\ C e. A /\ D e. 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 e. A /\ C e. A /\ D e. A ) ) -> -. ( B R C /\ C R D /\ D R B ) )