Metamath Proof Explorer


Theorem fr2nr

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

Ref Expression
Assertion fr2nr
|- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )

Proof

Step Hyp Ref Expression
1 prex
 |-  { B , C } e. _V
2 1 a1i
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } e. _V )
3 simpl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> R Fr A )
4 prssi
 |-  ( ( B e. A /\ C e. A ) -> { B , C } C_ A )
5 4 adantl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } C_ A )
6 prnzg
 |-  ( B e. A -> { B , C } =/= (/) )
7 6 ad2antrl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } =/= (/) )
8 fri
 |-  ( ( ( { B , C } e. _V /\ R Fr A ) /\ ( { B , C } C_ A /\ { B , C } =/= (/) ) ) -> E. y e. { B , C } A. x e. { B , C } -. x R y )
9 2 3 5 7 8 syl22anc
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> E. y e. { B , C } A. x e. { B , C } -. x R y )
10 breq2
 |-  ( y = B -> ( x R y <-> x R B ) )
11 10 notbid
 |-  ( y = B -> ( -. x R y <-> -. x R B ) )
12 11 ralbidv
 |-  ( y = B -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R B ) )
13 breq2
 |-  ( y = C -> ( x R y <-> x R C ) )
14 13 notbid
 |-  ( y = C -> ( -. x R y <-> -. x R C ) )
15 14 ralbidv
 |-  ( y = C -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R C ) )
16 12 15 rexprg
 |-  ( ( B e. A /\ C e. A ) -> ( E. y e. { B , C } A. x e. { B , C } -. x R y <-> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) ) )
17 16 adantl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( E. y e. { B , C } A. x e. { B , C } -. x R y <-> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) ) )
18 9 17 mpbid
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) )
19 prid2g
 |-  ( C e. A -> C e. { B , C } )
20 19 ad2antll
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> C e. { B , C } )
21 breq1
 |-  ( x = C -> ( x R B <-> C R B ) )
22 21 notbid
 |-  ( x = C -> ( -. x R B <-> -. C R B ) )
23 22 rspcv
 |-  ( C e. { B , C } -> ( A. x e. { B , C } -. x R B -> -. C R B ) )
24 20 23 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R B -> -. C R B ) )
25 prid1g
 |-  ( B e. A -> B e. { B , C } )
26 25 ad2antrl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> B e. { B , C } )
27 breq1
 |-  ( x = B -> ( x R C <-> B R C ) )
28 27 notbid
 |-  ( x = B -> ( -. x R C <-> -. B R C ) )
29 28 rspcv
 |-  ( B e. { B , C } -> ( A. x e. { B , C } -. x R C -> -. B R C ) )
30 26 29 syl
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R C -> -. B R C ) )
31 24 30 orim12d
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( ( A. x e. { B , C } -. x R B \/ A. x e. { B , C } -. x R C ) -> ( -. C R B \/ -. B R C ) ) )
32 18 31 mpd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. C R B \/ -. B R C ) )
33 32 orcomd
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. B R C \/ -. C R B ) )
34 ianor
 |-  ( -. ( B R C /\ C R B ) <-> ( -. B R C \/ -. C R B ) )
35 33 34 sylibr
 |-  ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )