This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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