Theorem fr2nr 2177

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

Assertion

Ref	Expression
fr2nr	|- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))

Proof of Theorem fr2nr

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 |- y e. V
2	1	prnz 1847	. . . . 5 |- -. {y, x} = (/)
3		zfpair 1891	. . . . . . 7 |- {y, x} e. V
4	3	frc 2172	. . . . . 6 |- (R Fr A -> (({y, x} (_ A /\ -. {y, x} = (/)) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/)))
5		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (w = y -> (zRw <-> zRy))
6	5	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (w = y -> {z | zRw} = {z | zRy})
7	6	ineq2d 1645	. . . . . . . . . . . . . . 15 |- (w = y -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRy}))
8	7	cleq1d 1109	. . . . . . . . . . . . . 14 |- (w = y -> (({y, x} i^i {z | zRw}) = (/) <-> ({y, x} i^i {z | zRy}) = (/)))
9	8	negbid 463	. . . . . . . . . . . . 13 |- (w = y -> (-. ({y, x} i^i {z | zRw}) = (/) <-> -. ({y, x} i^i {z | zRy}) = (/)))
10		brab1 2096	. . . . . . . . . . . . . 14 |- (xRy <-> x e. {z | zRy})
11		visset 1350	. . . . . . . . . . . . . . . 16 |- x e. V
12	11	pri2 1842	. . . . . . . . . . . . . . 15 |- x e. {y, x}
13		inelcm 1742	. . . . . . . . . . . . . . 15 |- ((x e. {y, x} /\ x e. {z | zRy}) -> -. ({y, x} i^i {z | zRy}) = (/))
14	12, 13	mpan 518	. . . . . . . . . . . . . 14 |- (x e. {z | zRy} -> -. ({y, x} i^i {z | zRy}) = (/))
15	10, 14	sylbi 174	. . . . . . . . . . . . 13 |- (xRy -> -. ({y, x} i^i {z | zRy}) = (/))
16	9, 15	syl5bir 184	. . . . . . . . . . . 12 |- (w = y -> (xRy -> -. ({y, x} i^i {z | zRw}) = (/)))
17	16	com12 13	. . . . . . . . . . 11 |- (xRy -> (w = y -> -. ({y, x} i^i {z | zRw}) = (/)))
18		breq2 2066	. . . . . . . . . . . . . . . . 17 |- (w = x -> (zRw <-> zRx))
19	18	biabdv 1183	. . . . . . . . . . . . . . . 16 |- (w = x -> {z | zRw} = {z | zRx})
20	19	ineq2d 1645	. . . . . . . . . . . . . . 15 |- (w = x -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRx}))
21	20	cleq1d 1109	. . . . . . . . . . . . . 14 |- (w = x -> (({y, x} i^i {z | zRw}) = (/) <-> ({y, x} i^i {z | zRx}) = (/)))
22	21	negbid 463	. . . . . . . . . . . . 13 |- (w = x -> (-. ({y, x} i^i {z | zRw}) = (/) <-> -. ({y, x} i^i {z | zRx}) = (/)))
23		brab1 2096	. . . . . . . . . . . . . 14 |- (yRx <-> y e. {z | zRx})
24	1	pri1 1841	. . . . . . . . . . . . . . 15 |- y e. {y, x}
25		inelcm 1742	. . . . . . . . . . . . . . 15 |- ((y e. {y, x} /\ y e. {z | zRx}) -> -. ({y, x} i^i {z | zRx}) = (/))
26	24, 25	mpan 518	. . . . . . . . . . . . . 14 |- (y e. {z | zRx} -> -. ({y, x} i^i {z | zRx}) = (/))
27	23, 26	sylbi 174	. . . . . . . . . . . . 13 |- (yRx -> -. ({y, x} i^i {z | zRx}) = (/))
28	22, 27	syl5bir 184	. . . . . . . . . . . 12 |- (w = x -> (yRx -> -. ({y, x} i^i {z | zRw}) = (/)))
29	28	com12 13	. . . . . . . . . . 11 |- (yRx -> (w = x -> -. ({y, x} i^i {z | zRw}) = (/)))
30	17, 29	jaao 330	. . . . . . . . . 10 |- ((xRy /\ yRx) -> ((w = y \/ w = x) -> -. ({y, x} i^i {z | zRw}) = (/)))
31		visset 1350	. . . . . . . . . . 11 |- w e. V
32	31	elpr 1823	. . . . . . . . . 10 |- (w e. {y, x} <-> (w = y \/ w = x))
33	30, 32	syl5ib 181	. . . . . . . . 9 |- ((xRy /\ yRx) -> (w e. {y, x} -> -. ({y, x} i^i {z | zRw}) = (/)))
34	33	con3i 90	. . . . . . . 8 |- (-. (w e. {y, x} -> -. ({y, x} i^i {z | zRw}) = (/)) -> -. (xRy /\ yRx))
35	34	expi 125	. . . . . . 7 |- (w e. {y, x} -> (({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx)))
36	35	r19.23aiv 1284	. . . . . 6 |- (E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx))
37	4, 36	syl6 23	. . . . 5 |- (R Fr A -> (({y, x} (_ A /\ -. {y, x} = (/)) -> -. (xRy /\ yRx)))
38	2, 37	mpan2i 522	. . . 4 |- (R Fr A -> ({y, x} (_ A -> -. (xRy /\ yRx)))
39	1, 11	prss 1854	. . . 4 |- ((y e. A /\ x e. A) <-> {y, x} (_ A)
40	38, 39	syl5ib 181	. . 3 |- (R Fr A -> ((y e. A /\ x e. A) -> -. (xRy /\ yRx)))
41	40	ancomsd 335	. 2 |- (R Fr A -> ((x e. A /\ y e. A) -> -. (xRy /\ yRx)))
42	41	imp 277	1 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))

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

This theorem is referenced by:  efrn2lp 2181  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-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  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-op 1815  df-br 2063  df-fr 2169

metamath.org