Theorem fr3nr 2178

Description: A founded relation has no 3-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.

Assertion

Ref	Expression
fr3nr	|- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))

Proof of Theorem fr3nr

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 |- y e. V
2	1	tpnz 1848	. . . . 5 |- -. {y, z, x} = (/)
3		tpex 1952	. . . . . . 7 |- {y, z, x} e. V
4	3	frc 2172	. . . . . 6 |- (R Fr A -> (({y, z, x} (_ A /\ -. {y, z, x} = (/)) -> E.v e. {y, z, x} ({y, z, x} i^i {w | wRv}) = (/)))
5		3jao 632	. . . . . . . . . . 11 |- (((v = y -> -. ({y, z, x} i^i {w | wRv}) = (/)) /\ (v = z -> -. ({y, z, x} i^i {w | wRv}) = (/)) /\ (v = x -> -. ({y, z, x} i^i {w | wRv}) = (/))) -> ((v = y \/ v = z \/ v = x) -> -. ({y, z, x} i^i {w | wRv}) = (/)))
6		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (v = y -> (wRv <-> wRy))
7	6	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (v = y -> {w | wRv} = {w | wRy})
8	7	ineq2d 1645	. . . . . . . . . . . . . . 15 |- (v = y -> ({y, z, x} i^i {w | wRv}) = ({y, z, x} i^i {w | wRy}))
9	8	cleq1d 1109	. . . . . . . . . . . . . 14 |- (v = y -> (({y, z, x} i^i {w | wRv}) = (/) <-> ({y, z, x} i^i {w | wRy}) = (/)))
10	9	negbid 463	. . . . . . . . . . . . 13 |- (v = y -> (-. ({y, z, x} i^i {w | wRv}) = (/) <-> -. ({y, z, x} i^i {w | wRy}) = (/)))
11		brab1 2096	. . . . . . . . . . . . . 14 |- (xRy <-> x e. {w | wRy})
12		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
13	12	tpi3 1845	. . . . . . . . . . . . . . 15 |- x e. {y, z, x}
14		inelcm 1742	. . . . . . . . . . . . . . 15 |- ((x e. {y, z, x} /\ x e. {w | wRy}) -> -. ({y, z, x} i^i {w | wRy}) = (/))
15	13, 14	mpan 518	. . . . . . . . . . . . . 14 |- (x e. {w | wRy} -> -. ({y, z, x} i^i {w | wRy}) = (/))
16	11, 15	sylbi 174	. . . . . . . . . . . . 13 |- (xRy -> -. ({y, z, x} i^i {w | wRy}) = (/))
17	10, 16	syl5bir 184	. . . . . . . . . . . 12 |- (v = y -> (xRy -> -. ({y, z, x} i^i {w | wRv}) = (/)))
18	17	com12 13	. . . . . . . . . . 11 |- (xRy -> (v = y -> -. ({y, z, x} i^i {w | wRv}) = (/)))
19		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (v = z -> (wRv <-> wRz))
20	19	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (v = z -> {w | wRv} = {w | wRz})
21	20	ineq2d 1645	. . . . . . . . . . . . . . 15 |- (v = z -> ({y, z, x} i^i {w | wRv}) = ({y, z, x} i^i {w | wRz}))
22	21	cleq1d 1109	. . . . . . . . . . . . . 14 |- (v = z -> (({y, z, x} i^i {w | wRv}) = (/) <-> ({y, z, x} i^i {w | wRz}) = (/)))
23	22	negbid 463	. . . . . . . . . . . . 13 |- (v = z -> (-. ({y, z, x} i^i {w | wRv}) = (/) <-> -. ({y, z, x} i^i {w | wRz}) = (/)))
24		brab1 2096	. . . . . . . . . . . . . 14 |- (yRz <-> y e. {w | wRz})
25	1	tpi1 1843	. . . . . . . . . . . . . . 15 |- y e. {y, z, x}
26		inelcm 1742	. . . . . . . . . . . . . . 15 |- ((y e. {y, z, x} /\ y e. {w | wRz}) -> -. ({y, z, x} i^i {w | wRz}) = (/))
27	25, 26	mpan 518	. . . . . . . . . . . . . 14 |- (y e. {w | wRz} -> -. ({y, z, x} i^i {w | wRz}) = (/))
28	24, 27	sylbi 174	. . . . . . . . . . . . 13 |- (yRz -> -. ({y, z, x} i^i {w | wRz}) = (/))
29	23, 28	syl5bir 184	. . . . . . . . . . . 12 |- (v = z -> (yRz -> -. ({y, z, x} i^i {w | wRv}) = (/)))
30	29	com12 13	. . . . . . . . . . 11 |- (yRz -> (v = z -> -. ({y, z, x} i^i {w | wRv}) = (/)))
31		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (v = x -> (wRv <-> wRx))
32	31	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (v = x -> {w | wRv} = {w | wRx})
33	32	ineq2d 1645	. . . . . . . . . . . . . . 15 |- (v = x -> ({y, z, x} i^i {w | wRv}) = ({y, z, x} i^i {w | wRx}))
34	33	cleq1d 1109	. . . . . . . . . . . . . 14 |- (v = x -> (({y, z, x} i^i {w | wRv}) = (/) <-> ({y, z, x} i^i {w | wRx}) = (/)))
35	34	negbid 463	. . . . . . . . . . . . 13 |- (v = x -> (-. ({y, z, x} i^i {w | wRv}) = (/) <-> -. ({y, z, x} i^i {w | wRx}) = (/)))
36		brab1 2096	. . . . . . . . . . . . . 14 |- (zRx <-> z e. {w | wRx})
37		visset 1350	. . . . . . . . . . . . . . . 16 |- z e. V
38	37	tpi2 1844	. . . . . . . . . . . . . . 15 |- z e. {y, z, x}
39		inelcm 1742	. . . . . . . . . . . . . . 15 |- ((z e. {y, z, x} /\ z e. {w | wRx}) -> -. ({y, z, x} i^i {w | wRx}) = (/))
40	38, 39	mpan 518	. . . . . . . . . . . . . 14 |- (z e. {w | wRx} -> -. ({y, z, x} i^i {w | wRx}) = (/))
41	36, 40	sylbi 174	. . . . . . . . . . . . 13 |- (zRx -> -. ({y, z, x} i^i {w | wRx}) = (/))
42	35, 41	syl5bir 184	. . . . . . . . . . . 12 |- (v = x -> (zRx -> -. ({y, z, x} i^i {w | wRv}) = (/)))
43	42	com12 13	. . . . . . . . . . 11 |- (zRx -> (v = x -> -. ({y, z, x} i^i {w | wRv}) = (/)))
44	5, 18, 30, 43	syl3an 628	. . . . . . . . . 10 |- ((xRy /\ yRz /\ zRx) -> ((v = y \/ v = z \/ v = x) -> -. ({y, z, x} i^i {w | wRv}) = (/)))
45		visset 1350	. . . . . . . . . . 11 |- v e. V
46	45	eltp 1834	. . . . . . . . . 10 |- (v e. {y, z, x} <-> (v = y \/ v = z \/ v = x))
47	44, 46	syl5ib 181	. . . . . . . . 9 |- ((xRy /\ yRz /\ zRx) -> (v e. {y, z, x} -> -. ({y, z, x} i^i {w | wRv}) = (/)))
48	47	con3i 90	. . . . . . . 8 |- (-. (v e. {y, z, x} -> -. ({y, z, x} i^i {w | wRv}) = (/)) -> -. (xRy /\ yRz /\ zRx))
49	48	expi 125	. . . . . . 7 |- (v e. {y, z, x} -> (({y, z, x} i^i {w | wRv}) = (/) -> -. (xRy /\ yRz /\ zRx)))
50	49	r19.23aiv 1284	. . . . . 6 |- (E.v e. {y, z, x} ({y, z, x} i^i {w | wRv}) = (/) -> -. (xRy /\ yRz /\ zRx))
51	4, 50	syl6 23	. . . . 5 |- (R Fr A -> (({y, z, x} (_ A /\ -. {y, z, x} = (/)) -> -. (xRy /\ yRz /\ zRx)))
52	2, 51	mpan2i 522	. . . 4 |- (R Fr A -> ({y, z, x} (_ A -> -. (xRy /\ yRz /\ zRx)))
53	1, 37, 12	tpss 1855	. . . 4 |- ((y e. A /\ z e. A /\ x e. A) <-> {y, z, x} (_ A)
54	52, 53	syl5ib 181	. . 3 |- (R Fr A -> ((y e. A /\ z e. A /\ x e. A) -> -. (xRy /\ yRz /\ zRx)))
55		3anrot 586	. . 3 |- ((x e. A /\ y e. A /\ z e. A) <-> (y e. A /\ z e. A /\ x e. A))
56	54, 55	syl5ib 181	. 2 |- (R Fr A -> ((x e. A /\ y e. A /\ z e. A) -> -. (xRy /\ yRz /\ zRx)))
57	56	imp 277	1 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   \/ w3o 580   /\ w3a 581   = weq 797  {cab 1090   = wceq 1091   e. wcel 1092  E.wrex 1202   i^i cin 1486   (_ wss 1487  (/)c0 1707  {ctp 1813   class class class wbr 2054   Fr wfr 2061

This theorem is referenced by:  epne3 2182  dfwe2 2187

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ral 1205  df-rex 1206  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-br 2063  df-fr 2169

metamath.org