Theorem fr2nr 2922

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 1811	. . . . . 6 |- y e. V
2	1	prnz 2457	. . . . 5 |- {y, x} =/= (/)
3		zfpair2 2777	. . . . . 6 |- {y, x} e. V
4	3	frc 2917	. . . . 5 |- ((R Fr A /\ {y, x} (_ A /\ {y, x} =/= (/)) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
5	2, 4	mp3an3 904	. . . 4 |- ((R Fr A /\ {y, x} (_ A) -> E.w e. {y, x} ({y, x} i^i {z | zRw}) = (/))
6		breq2 2620	. . . . . . . . . . . . 13 |- (w = y -> (zRw <-> zRy))
7	6	abbidv 1576	. . . . . . . . . . . 12 |- (w = y -> {z | zRw} = {z | zRy})
8	7	ineq2d 2215	. . . . . . . . . . 11 |- (w = y -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRy}))
9	8	neeq1d 1593	. . . . . . . . . 10 |- (w = y -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRy}) =/= (/)))
10		brab1 2657	. . . . . . . . . . 11 |- (xRy <-> x e. {z | zRy})
11		visset 1811	. . . . . . . . . . . . 13 |- x e. V
12	11	pri2 2449	. . . . . . . . . . . 12 |- x e. {y, x}
13		inelcm 2321	. . . . . . . . . . . 12 |- ((x e. {y, x} /\ x e. {z | zRy}) -> ({y, x} i^i {z | zRy}) =/= (/))
14	12, 13	mpan 694	. . . . . . . . . . 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 2620	. . . . . . . . . . . . 13 |- (w = x -> (zRw <-> zRx))
18	17	abbidv 1576	. . . . . . . . . . . 12 |- (w = x -> {z | zRw} = {z | zRx})
19	18	ineq2d 2215	. . . . . . . . . . 11 |- (w = x -> ({y, x} i^i {z | zRw}) = ({y, x} i^i {z | zRx}))
20	19	neeq1d 1593	. . . . . . . . . 10 |- (w = x -> (({y, x} i^i {z | zRw}) =/= (/) <-> ({y, x} i^i {z | zRx}) =/= (/)))
21		brab1 2657	. . . . . . . . . . 11 |- (yRx <-> y e. {z | zRx})
22	1	pri1 2448	. . . . . . . . . . . 12 |- y e. {y, x}
23		inelcm 2321	. . . . . . . . . . . 12 |- ((y e. {y, x} /\ y e. {z | zRx}) -> ({y, x} i^i {z | zRx}) =/= (/))
24	22, 23	mpan 694	. . . . . . . . . . 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 1811	. . . . . . . . 9 |- w e. V
29	28	elpr 2422	. . . . . . . 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 1614	. . . . 5 |- (w e. {y, x} -> (({y, x} i^i {z | zRw}) = (/) -> -. (xRy /\ yRx)))
33	32	r19.23aiv 1742	. . . 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 2469	. . 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 487	1 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223   = wceq 955   e. wcel 957  {cab 1463   =/= wne 1584  E.wrex 1645   i^i cin 2044   (_ wss 2045  (/)c0 2278  {cpr 2408   class class class wbr 2616   Fr wfr 2912

This theorem is referenced by:  efrn2lp 2926  dfwe2 2932

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2700  ax-pr 2776

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 776  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1586  df-ral 1648  df-rex 1649  df-v 1810  df-dif 2047  df-un 2048  df-in 2049  df-ss 2051  df-nul 2279  df-sn 2410  df-pr 2411  df-op 2414  df-br 2617  df-fr 2914

Copyright terms: Public domain