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