Theorem fr2nr 2915

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 1804	. . . . . 6 |- y e. V
2	1	prnz 2450	. . . . 5 |- {y, x} =/= (/)
3		zfpair2 2770	. . . . . 6 |- {y, x} e. V
4	3	frc 2910	. . . . 5 |- ((R Fr A /\ {y, x} (_ A /\ {y, x} =/= (/)) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
5	2, 4	mp3an3 902	. . . 4 |- ((R Fr A /\ {y, x} (_ A) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
6		breq2 2613	. . . . . . . . . . . . 13 |- (w = y -> (zRw <-> zRy))
7	6	abbidv 1569	. . . . . . . . . . . 12 |- (w = y -> {z | zRw} = {z | zRy})
8	7	ineq2d 2207	. . . . . . . . . . 11 |- (w = y -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRy}))
9	8	neeq1d 1586	. . . . . . . . . 10 |- (w = y -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRy}) =/= (/)))
10		brab1 2650	. . . . . . . . . . 11 |- (xRy <-> x e. {z | zRy})
11		visset 1804	. . . . . . . . . . . . 13 |- x e. V
12	11	pri2 2442	. . . . . . . . . . . 12 |- x e. {y, x}
13		inelcm 2313	. . . . . . . . . . . 12 |- ((x e. {y, x} /\ x e. {z | zRy}) -> ({y, x} i^i {z | zRy}) =/= (/))
14	12, 13	mpan 693	. . . . . . . . . . 11 |- (x e. {z | zRy} -> ({y, x} i^i {z | zRy}) =/= (/))
15	10, 14	sylbi 199	. . . . . . . . . 10 |- (xRy -> ({y, x} i^i {z | zRy}) =/= (/))
16	9, 15	syl5cbir 211	. . . . . . . . 9 |- (xRy -> (w = y -> ({y, x} i^i {z | zRw}) =/= (/)))
17		breq2 2613	. . . . . . . . . . . . 13 |- (w = x -> (zRw <-> zRx))
18	17	abbidv 1569	. . . . . . . . . . . 12 |- (w = x -> {z | zRw} = {z | zRx})
19	18	ineq2d 2207	. . . . . . . . . . 11 |- (w = x -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRx}))
20	19	neeq1d 1586	. . . . . . . . . 10 |- (w = x -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRx}) =/= (/)))
21		brab1 2650	. . . . . . . . . . 11 |- (yRx <-> y e. {z | zRx})
22	1	pri1 2441	. . . . . . . . . . . 12 |- y e. {y, x}
23		inelcm 2313	. . . . . . . . . . . 12 |- ((y e. {y, x} /\ y e. {z | zRx}) -> ({y, x} i^i {z | zRx}) =/= (/))
24	22, 23	mpan 693	. . . . . . . . . . 11 |- (y e. {z | zRx} -> ({y, x} i^i {z | zRx}) =/= (/))
25	21, 24	sylbi 199	. . . . . . . . . 10 |- (yRx -> ({y, x} i^i {z | zRx}) =/= (/))
26	20, 25	syl5cbir 211	. . . . . . . . 9 |- (yRx -> (w = x -> ({y, x} i^i {z | zRw}) =/= (/)))
27	16, 26	jaao 427	. . . . . . . 8 |- ((xRy /\ yRx) -> ((w = y \/ w = x) -> ({y, x} i^i {z | zRw}) =/= (/)))
28		visset 1804	. . . . . . . . 9 |- w e. V
29	28	elpr 2414	. . . . . . . 8 |- (w e. {y, x} <-> (w = y \/ w = x))
30	27, 29	syl5ib 206	. . . . . . 7 |- ((xRy /\ yRx) -> (w e. {y, x} -> ({y, x} i^i {z | zRw}) =/= (/)))
31	30	com12 11	. . . . . 6 |- (w e. {y, x} -> ((xRy /\ yRx) -> ({y, x} i^i {z | zRw}) =/= (/)))
32	31	necon2bd 1607	. . . . 5 |- (w e. {y, x} -> (({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx)))
33	32	r19.23aiv 1735	. . . 4 |- (E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx))
34	5, 33	syl 10	. . 3 |- ((R Fr A /\ {y, x} (_ A) -> -. (xRy /\ yRx))
35	1, 11	prss 2462	. . 3 |- ((y e. A /\ x e. A) <-> {y, x} (_ A)
36	34, 35	sylan2b 452	. 2 |- ((R Fr A /\ (y e. A /\ x e. A)) -> -. (xRy /\ yRx))
37	36	ancom2s 486	1 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   = wceq 953   e. wcel 955  {cab 1456   =/= wne 1577  E.wrex 1638   i^i cin 2036   (_ wss 2037  (/)c0 2270  {cpr 2400   class class class wbr 2609   Fr wfr 2905

This theorem is referenced by:  efrn2lp 2919  dfwe2 2925

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pr 2769

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610  df-fr 2907

Copyright terms: Public domain