Theorem fr2nr 2980

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 1851	. . . . . 6 |- y e. V
2	1	prnz 2507	. . . . 5 |- {y, x} =/= (/)
3		zfpair2 2833	. . . . . 6 |- {y, x} e. V
4	3	frc 2975	. . . . 5 |- ((R Fr A /\ {y, x} (_ A /\ {y, x} =/= (/)) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
5	2, 4	mp3an3 908	. . . 4 |- ((R Fr A /\ {y, x} (_ A) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
6		breq2 2673	. . . . . . . . . . . . 13 |- (w = y -> (zRw <-> zRy))
7	6	abbidv 1614	. . . . . . . . . . . 12 |- (w = y -> {z | zRw} = {z | zRy})
8	7	ineq2d 2261	. . . . . . . . . . 11 |- (w = y -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRy}))
9	8	neeq1d 1631	. . . . . . . . . 10 |- (w = y -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRy}) =/= (/)))
10		brab1 2710	. . . . . . . . . . 11 |- (xRy <-> x e. {z | zRy})
11		visset 1851	. . . . . . . . . . . . 13 |- x e. V
12	11	prid2 2498	. . . . . . . . . . . 12 |- x e. {y, x}
13		inelcm 2368	. . . . . . . . . . . 12 |- ((x e. {y, x} /\ x e. {z | zRy}) -> ({y, x} i^i {z | zRy}) =/= (/))
14	12, 13	mpan 698	. . . . . . . . . . 11 |- (x e. {z | zRy} -> ({y, x} i^i {z | zRy}) =/= (/))
15	10, 14	sylbi 197	. . . . . . . . . 10 |- (xRy -> ({y, x} i^i {z | zRy}) =/= (/))
16	9, 15	syl5cbir 209	. . . . . . . . 9 |- (xRy -> (w = y -> ({y, x} i^i {z | zRw}) =/= (/)))
17		breq2 2673	. . . . . . . . . . . . 13 |- (w = x -> (zRw <-> zRx))
18	17	abbidv 1614	. . . . . . . . . . . 12 |- (w = x -> {z | zRw} = {z | zRx})
19	18	ineq2d 2261	. . . . . . . . . . 11 |- (w = x -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRx}))
20	19	neeq1d 1631	. . . . . . . . . 10 |- (w = x -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRx}) =/= (/)))
21		brab1 2710	. . . . . . . . . . 11 |- (yRx <-> y e. {z | zRx})
22	1	prid1 2497	. . . . . . . . . . . 12 |- y e. {y, x}
23		inelcm 2368	. . . . . . . . . . . 12 |- ((y e. {y, x} /\ y e. {z | zRx}) -> ({y, x} i^i {z | zRx}) =/= (/))
24	22, 23	mpan 698	. . . . . . . . . . 11 |- (y e. {z | zRx} -> ({y, x} i^i {z | zRx}) =/= (/))
25	21, 24	sylbi 197	. . . . . . . . . 10 |- (yRx -> ({y, x} i^i {z | zRx}) =/= (/))
26	20, 25	syl5cbir 209	. . . . . . . . 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 1851	. . . . . . . . 9 |- w e. V
29	28	elpr 2469	. . . . . . . 8 |- (w e. {y, x} <-> (w = y \/ w = x))
30	27, 29	syl5ib 204	. . . . . . 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 1652	. . . . 5 |- (w e. {y, x} -> (({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx)))
33	32	r19.23aiv 1781	. . . 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 2519	. . 3 |- ((y e. A /\ x e. A) <-> {y, x} (_ A)
36	34, 35	sylan2b 454	. 2 |- ((R Fr A /\ (y e. A /\ x e. A)) -> -. (xRy /\ yRx))
37	36	ancom2s 489	1 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 220   /\ wa 221   = wceq 988   e. wcel 990  {cab 1499   =/= wne 1622  E.wrex 1684   i^i cin 2090   (_ wss 2091  (/)c0 2324  {cpr 2455   class class class wbr 2669   Fr wfr 2970

This theorem is referenced by:  efrn2lp 2984  dfwe2 2990

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 780  df-ex 1013  df-sb 1205  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-rex 1688  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-fr 2972

Copyright terms: Public domain