Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fr3nr Structured version   Unicode version

Theorem fr3nr 6564
 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.)
Assertion
Ref Expression
fr3nr

Proof of Theorem fr3nr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tpex 6548 . . . . . . 7
21a1i 11 . . . . . 6
3 simpl 458 . . . . . 6
4 df-tp 3946 . . . . . . 7
5 simpr1 1011 . . . . . . . . 9
6 simpr2 1012 . . . . . . . . 9
7 prssi 4099 . . . . . . . . 9
85, 6, 7syl2anc 665 . . . . . . . 8
9 simpr3 1013 . . . . . . . . 9
109snssd 4088 . . . . . . . 8
118, 10unssd 3585 . . . . . . 7
124, 11syl5eqss 3451 . . . . . 6
135tpnzd 4065 . . . . . 6
14 fri 4758 . . . . . 6
152, 3, 12, 13, 14syl22anc 1265 . . . . 5
16 breq2 4370 . . . . . . . . 9
1716notbid 295 . . . . . . . 8
1817ralbidv 2804 . . . . . . 7
19 breq2 4370 . . . . . . . . 9
2019notbid 295 . . . . . . . 8
2120ralbidv 2804 . . . . . . 7
22 breq2 4370 . . . . . . . . 9
2322notbid 295 . . . . . . . 8
2423ralbidv 2804 . . . . . . 7
2518, 21, 24rextpg 3995 . . . . . 6
2625adantl 467 . . . . 5
2715, 26mpbid 213 . . . 4
28 snsstp3 4096 . . . . . . 7
29 snssg 4076 . . . . . . . 8
309, 29syl 17 . . . . . . 7
3128, 30mpbiri 236 . . . . . 6
32 breq1 4369 . . . . . . . 8
3332notbid 295 . . . . . . 7
3433rspcv 3121 . . . . . 6
3531, 34syl 17 . . . . 5
36 snsstp1 4094 . . . . . . 7
37 snssg 4076 . . . . . . . 8
385, 37syl 17 . . . . . . 7
3936, 38mpbiri 236 . . . . . 6
40 breq1 4369 . . . . . . . 8
4140notbid 295 . . . . . . 7
4241rspcv 3121 . . . . . 6
4339, 42syl 17 . . . . 5
44 snsstp2 4095 . . . . . . 7
45 snssg 4076 . . . . . . . 8
466, 45syl 17 . . . . . . 7
4744, 46mpbiri 236 . . . . . 6
48 breq1 4369 . . . . . . . 8
4948notbid 295 . . . . . . 7
5049rspcv 3121 . . . . . 6
5147, 50syl 17 . . . . 5
5235, 43, 513orim123d 1343 . . . 4
5327, 52mpd 15 . . 3
54 3ianor 999 . . 3
5553, 54sylibr 215 . 2
56 3anrot 987 . 2
5755, 56sylnib 305 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3o 981   w3a 982   wceq 1437   wcel 1872   wne 2599  wral 2714  wrex 2715  cvv 3022   cun 3377   wss 3379  c0 3704  csn 3941  cpr 3943  ctp 3945   class class class wbr 4366   wfr 4752 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603  ax-un 6541 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-br 4367  df-fr 4755 This theorem is referenced by:  epne3  6565  dfwe2  6566
 Copyright terms: Public domain W3C validator