Theorem fr2nr 5092

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

Assertion

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

Proof of Theorem fr2nr

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prex 4909	. . . . . . 7 |- { B , C } e. _V
2	1	a1i 11	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } e. _V )
3		simpl 473	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> R Fr A )
4		prssi 4353	. . . . . . 7 |- ( ( B e. A /\ C e. A ) -> { B , C } C_ A )
5	4	adantl 482	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } C_ A )
6		prnzg 4311	. . . . . . 7 |- ( B e. A -> { B , C } =/= (/) )
7	6	ad2antrl 764	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> { B , C } =/= (/) )
8		fri 5076	. . . . . 6 |- ( ( ( { 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 1327	. . . . 5 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> E. y e. { B , C } A. x e. { B , C } -. x R y )
10		breq2 4657	. . . . . . . . 9 |- ( y = B -> ( x R y <-> x R B ) )
11	10	notbid 308	. . . . . . . 8 |- ( y = B -> ( -. x R y <-> -. x R B ) )
12	11	ralbidv 2986	. . . . . . 7 |- ( y = B -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R B ) )
13		breq2 4657	. . . . . . . . 9 |- ( y = C -> ( x R y <-> x R C ) )
14	13	notbid 308	. . . . . . . 8 |- ( y = C -> ( -. x R y <-> -. x R C ) )
15	14	ralbidv 2986	. . . . . . 7 |- ( y = C -> ( A. x e. { B , C } -. x R y <-> A. x e. { B , C } -. x R C ) )
16	12, 15	rexprg 4235	. . . . . 6 |- ( ( 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 482	. . . . 5 |- ( ( 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 222	. . . 4 |- ( ( 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 4296	. . . . . . 7 |- ( C e. A -> C e. { B , C } )
20	19	ad2antll 765	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> C e. { B , C } )
21		breq1 4656	. . . . . . . 8 |- ( x = C -> ( x R B <-> C R B ) )
22	21	notbid 308	. . . . . . 7 |- ( x = C -> ( -. x R B <-> -. C R B ) )
23	22	rspcv 3305	. . . . . 6 |- ( C e. { B , C } -> ( A. x e. { B , C } -. x R B -> -. C R B ) )
24	20, 23	syl 17	. . . . 5 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R B -> -. C R B ) )
25		prid1g 4295	. . . . . . 7 |- ( B e. A -> B e. { B , C } )
26	25	ad2antrl 764	. . . . . 6 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> B e. { B , C } )
27		breq1 4656	. . . . . . . 8 |- ( x = B -> ( x R C <-> B R C ) )
28	27	notbid 308	. . . . . . 7 |- ( x = B -> ( -. x R C <-> -. B R C ) )
29	28	rspcv 3305	. . . . . 6 |- ( B e. { B , C } -> ( A. x e. { B , C } -. x R C -> -. B R C ) )
30	26, 29	syl 17	. . . . 5 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( A. x e. { B , C } -. x R C -> -. B R C ) )
31	24, 30	orim12d 883	. . . 4 |- ( ( 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 15	. . 3 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. C R B \/ -. B R C ) )
33	32	orcomd 403	. 2 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> ( -. B R C \/ -. C R B ) )
34		ianor 509	. 2 |- ( -. ( B R C /\ C R B ) <-> ( -. B R C \/ -. C R B ) )
35	33, 34	sylibr 224	1 |- ( ( R Fr A /\ ( B e. A /\ C e. A ) ) -> -. ( B R C /\ C R B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   C_ wss 3574   (/)c0 3915   {cpr 4179   class class class wbr 4653   Fr wfr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-fr 5073

This theorem is referenced by:  efrn2lp  5096  dfwe2  6981