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 ∈ A ∧ y ∈ A)) → ¬ (xRy ∧ yRx))

Proof of Theorem fr2nr

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 ⊢ y ∈ V
2	1	prnz 1847	. . . . 5 ⊢ ¬ {y, x} = ∅
3		zfpair 1891	. . . . . . 7 ⊢ {y, x} ∈ V
4	3	frc 2172	. . . . . 6 ⊢ (R Fr A → (({y, x} ⊆ A ∧ ¬ {y, x} = ∅) → ∃w ∈ {y, x} ({y, x} ∩ {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} ∩ {z∣zRw}) = ({y, x} ∩ {z∣zRy}))
8	7	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (w = y → (({y, x} ∩ {z∣zRw}) = ∅ ↔ ({y, x} ∩ {z∣zRy}) = ∅))
9	8	negbid 463	. . . . . . . . . . . . 13 ⊢ (w = y → (¬ ({y, x} ∩ {z∣zRw}) = ∅ ↔ ¬ ({y, x} ∩ {z∣zRy}) = ∅))
10		brab1 2096	. . . . . . . . . . . . . 14 ⊢ (xRy ↔ x ∈ {z∣zRy})
11		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
12	11	pri2 1842	. . . . . . . . . . . . . . 15 ⊢ x ∈ {y, x}
13		inelcm 1742	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ {y, x} ∧ x ∈ {z∣zRy}) → ¬ ({y, x} ∩ {z∣zRy}) = ∅)
14	12, 13	mpan 518	. . . . . . . . . . . . . 14 ⊢ (x ∈ {z∣zRy} → ¬ ({y, x} ∩ {z∣zRy}) = ∅)
15	10, 14	sylbi 174	. . . . . . . . . . . . 13 ⊢ (xRy → ¬ ({y, x} ∩ {z∣zRy}) = ∅)
16	9, 15	syl5bir 184	. . . . . . . . . . . 12 ⊢ (w = y → (xRy → ¬ ({y, x} ∩ {z∣zRw}) = ∅))
17	16	com12 13	. . . . . . . . . . 11 ⊢ (xRy → (w = y → ¬ ({y, x} ∩ {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} ∩ {z∣zRw}) = ({y, x} ∩ {z∣zRx}))
21	20	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (w = x → (({y, x} ∩ {z∣zRw}) = ∅ ↔ ({y, x} ∩ {z∣zRx}) = ∅))
22	21	negbid 463	. . . . . . . . . . . . 13 ⊢ (w = x → (¬ ({y, x} ∩ {z∣zRw}) = ∅ ↔ ¬ ({y, x} ∩ {z∣zRx}) = ∅))
23		brab1 2096	. . . . . . . . . . . . . 14 ⊢ (yRx ↔ y ∈ {z∣zRx})
24	1	pri1 1841	. . . . . . . . . . . . . . 15 ⊢ y ∈ {y, x}
25		inelcm 1742	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ {y, x} ∧ y ∈ {z∣zRx}) → ¬ ({y, x} ∩ {z∣zRx}) = ∅)
26	24, 25	mpan 518	. . . . . . . . . . . . . 14 ⊢ (y ∈ {z∣zRx} → ¬ ({y, x} ∩ {z∣zRx}) = ∅)
27	23, 26	sylbi 174	. . . . . . . . . . . . 13 ⊢ (yRx → ¬ ({y, x} ∩ {z∣zRx}) = ∅)
28	22, 27	syl5bir 184	. . . . . . . . . . . 12 ⊢ (w = x → (yRx → ¬ ({y, x} ∩ {z∣zRw}) = ∅))
29	28	com12 13	. . . . . . . . . . 11 ⊢ (yRx → (w = x → ¬ ({y, x} ∩ {z∣zRw}) = ∅))
30	17, 29	jaao 330	. . . . . . . . . 10 ⊢ ((xRy ∧ yRx) → ((w = y ∨ w = x) → ¬ ({y, x} ∩ {z∣zRw}) = ∅))
31		visset 1350	. . . . . . . . . . 11 ⊢ w ∈ V
32	31	elpr 1823	. . . . . . . . . 10 ⊢ (w ∈ {y, x} ↔ (w = y ∨ w = x))
33	30, 32	syl5ib 181	. . . . . . . . 9 ⊢ ((xRy ∧ yRx) → (w ∈ {y, x} → ¬ ({y, x} ∩ {z∣zRw}) = ∅))
34	33	con3i 90	. . . . . . . 8 ⊢ (¬ (w ∈ {y, x} → ¬ ({y, x} ∩ {z∣zRw}) = ∅) → ¬ (xRy ∧ yRx))
35	34	expi 125	. . . . . . 7 ⊢ (w ∈ {y, x} → (({y, x} ∩ {z∣zRw}) = ∅ → ¬ (xRy ∧ yRx)))
36	35	r19.23aiv 1284	. . . . . 6 ⊢ (∃w ∈ {y, x} ({y, x} ∩ {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 ∈ A ∧ x ∈ A) ↔ {y, x} ⊆ A)
40	38, 39	syl5ib 181	. . 3 ⊢ (R Fr A → ((y ∈ A ∧ x ∈ A) → ¬ (xRy ∧ yRx)))
41	40	ancomsd 335	. 2 ⊢ (R Fr A → ((x ∈ A ∧ y ∈ A) → ¬ (xRy ∧ yRx)))
42	41	imp 277	1 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A)) → ¬ (xRy ∧ yRx))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202   ∩ 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