Theorem fr3nr 2178

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

Assertion

Ref	Expression
fr3nr	⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (xRy ∧ yRz ∧ zRx))

Proof of Theorem fr3nr

Step	Hyp	Ref	Expression
1		visset 1350	. . . . . 6 ⊢ y ∈ V
2	1	tpnz 1848	. . . . 5 ⊢ ¬ {y, z, x} = ∅
3		tpex 1952	. . . . . . 7 ⊢ {y, z, x} ∈ V
4	3	frc 2172	. . . . . 6 ⊢ (R Fr A → (({y, z, x} ⊆ A ∧ ¬ {y, z, x} = ∅) → ∃v ∈ {y, z, x} ({y, z, x} ∩ {w∣wRv}) = ∅))
5		3jao 632	. . . . . . . . . . 11 ⊢ (((v = y → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅) ∧ (v = z → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅) ∧ (v = x → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅)) → ((v = y ∨ v = z ∨ v = x) → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
6		breq2 2066	. . . . . . . . . . . . . . . . 17 ⊢ (v = y → (wRv ↔ wRy))
7	6	biabdv 1183	. . . . . . . . . . . . . . . 16 ⊢ (v = y → {w∣wRv} = {w∣wRy})
8	7	ineq2d 1645	. . . . . . . . . . . . . . 15 ⊢ (v = y → ({y, z, x} ∩ {w∣wRv}) = ({y, z, x} ∩ {w∣wRy}))
9	8	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (v = y → (({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ({y, z, x} ∩ {w∣wRy}) = ∅))
10	9	negbid 463	. . . . . . . . . . . . 13 ⊢ (v = y → (¬ ({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ¬ ({y, z, x} ∩ {w∣wRy}) = ∅))
11		brab1 2096	. . . . . . . . . . . . . 14 ⊢ (xRy ↔ x ∈ {w∣wRy})
12		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ x ∈ V
13	12	tpi3 1845	. . . . . . . . . . . . . . 15 ⊢ x ∈ {y, z, x}
14		inelcm 1742	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ {y, z, x} ∧ x ∈ {w∣wRy}) → ¬ ({y, z, x} ∩ {w∣wRy}) = ∅)
15	13, 14	mpan 518	. . . . . . . . . . . . . 14 ⊢ (x ∈ {w∣wRy} → ¬ ({y, z, x} ∩ {w∣wRy}) = ∅)
16	11, 15	sylbi 174	. . . . . . . . . . . . 13 ⊢ (xRy → ¬ ({y, z, x} ∩ {w∣wRy}) = ∅)
17	10, 16	syl5bir 184	. . . . . . . . . . . 12 ⊢ (v = y → (xRy → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
18	17	com12 13	. . . . . . . . . . 11 ⊢ (xRy → (v = y → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
19		breq2 2066	. . . . . . . . . . . . . . . . 17 ⊢ (v = z → (wRv ↔ wRz))
20	19	biabdv 1183	. . . . . . . . . . . . . . . 16 ⊢ (v = z → {w∣wRv} = {w∣wRz})
21	20	ineq2d 1645	. . . . . . . . . . . . . . 15 ⊢ (v = z → ({y, z, x} ∩ {w∣wRv}) = ({y, z, x} ∩ {w∣wRz}))
22	21	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (v = z → (({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ({y, z, x} ∩ {w∣wRz}) = ∅))
23	22	negbid 463	. . . . . . . . . . . . 13 ⊢ (v = z → (¬ ({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ¬ ({y, z, x} ∩ {w∣wRz}) = ∅))
24		brab1 2096	. . . . . . . . . . . . . 14 ⊢ (yRz ↔ y ∈ {w∣wRz})
25	1	tpi1 1843	. . . . . . . . . . . . . . 15 ⊢ y ∈ {y, z, x}
26		inelcm 1742	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ {y, z, x} ∧ y ∈ {w∣wRz}) → ¬ ({y, z, x} ∩ {w∣wRz}) = ∅)
27	25, 26	mpan 518	. . . . . . . . . . . . . 14 ⊢ (y ∈ {w∣wRz} → ¬ ({y, z, x} ∩ {w∣wRz}) = ∅)
28	24, 27	sylbi 174	. . . . . . . . . . . . 13 ⊢ (yRz → ¬ ({y, z, x} ∩ {w∣wRz}) = ∅)
29	23, 28	syl5bir 184	. . . . . . . . . . . 12 ⊢ (v = z → (yRz → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
30	29	com12 13	. . . . . . . . . . 11 ⊢ (yRz → (v = z → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
31		breq2 2066	. . . . . . . . . . . . . . . . 17 ⊢ (v = x → (wRv ↔ wRx))
32	31	biabdv 1183	. . . . . . . . . . . . . . . 16 ⊢ (v = x → {w∣wRv} = {w∣wRx})
33	32	ineq2d 1645	. . . . . . . . . . . . . . 15 ⊢ (v = x → ({y, z, x} ∩ {w∣wRv}) = ({y, z, x} ∩ {w∣wRx}))
34	33	cleq1d 1109	. . . . . . . . . . . . . 14 ⊢ (v = x → (({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ({y, z, x} ∩ {w∣wRx}) = ∅))
35	34	negbid 463	. . . . . . . . . . . . 13 ⊢ (v = x → (¬ ({y, z, x} ∩ {w∣wRv}) = ∅ ↔ ¬ ({y, z, x} ∩ {w∣wRx}) = ∅))
36		brab1 2096	. . . . . . . . . . . . . 14 ⊢ (zRx ↔ z ∈ {w∣wRx})
37		visset 1350	. . . . . . . . . . . . . . . 16 ⊢ z ∈ V
38	37	tpi2 1844	. . . . . . . . . . . . . . 15 ⊢ z ∈ {y, z, x}
39		inelcm 1742	. . . . . . . . . . . . . . 15 ⊢ ((z ∈ {y, z, x} ∧ z ∈ {w∣wRx}) → ¬ ({y, z, x} ∩ {w∣wRx}) = ∅)
40	38, 39	mpan 518	. . . . . . . . . . . . . 14 ⊢ (z ∈ {w∣wRx} → ¬ ({y, z, x} ∩ {w∣wRx}) = ∅)
41	36, 40	sylbi 174	. . . . . . . . . . . . 13 ⊢ (zRx → ¬ ({y, z, x} ∩ {w∣wRx}) = ∅)
42	35, 41	syl5bir 184	. . . . . . . . . . . 12 ⊢ (v = x → (zRx → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
43	42	com12 13	. . . . . . . . . . 11 ⊢ (zRx → (v = x → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
44	5, 18, 30, 43	syl3an 628	. . . . . . . . . 10 ⊢ ((xRy ∧ yRz ∧ zRx) → ((v = y ∨ v = z ∨ v = x) → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
45		visset 1350	. . . . . . . . . . 11 ⊢ v ∈ V
46	45	eltp 1834	. . . . . . . . . 10 ⊢ (v ∈ {y, z, x} ↔ (v = y ∨ v = z ∨ v = x))
47	44, 46	syl5ib 181	. . . . . . . . 9 ⊢ ((xRy ∧ yRz ∧ zRx) → (v ∈ {y, z, x} → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅))
48	47	con3i 90	. . . . . . . 8 ⊢ (¬ (v ∈ {y, z, x} → ¬ ({y, z, x} ∩ {w∣wRv}) = ∅) → ¬ (xRy ∧ yRz ∧ zRx))
49	48	expi 125	. . . . . . 7 ⊢ (v ∈ {y, z, x} → (({y, z, x} ∩ {w∣wRv}) = ∅ → ¬ (xRy ∧ yRz ∧ zRx)))
50	49	r19.23aiv 1284	. . . . . 6 ⊢ (∃v ∈ {y, z, x} ({y, z, x} ∩ {w∣wRv}) = ∅ → ¬ (xRy ∧ yRz ∧ zRx))
51	4, 50	syl6 23	. . . . 5 ⊢ (R Fr A → (({y, z, x} ⊆ A ∧ ¬ {y, z, x} = ∅) → ¬ (xRy ∧ yRz ∧ zRx)))
52	2, 51	mpan2i 522	. . . 4 ⊢ (R Fr A → ({y, z, x} ⊆ A → ¬ (xRy ∧ yRz ∧ zRx)))
53	1, 37, 12	tpss 1855	. . . 4 ⊢ ((y ∈ A ∧ z ∈ A ∧ x ∈ A) ↔ {y, z, x} ⊆ A)
54	52, 53	syl5ib 181	. . 3 ⊢ (R Fr A → ((y ∈ A ∧ z ∈ A ∧ x ∈ A) → ¬ (xRy ∧ yRz ∧ zRx)))
55		3anrot 586	. . 3 ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) ↔ (y ∈ A ∧ z ∈ A ∧ x ∈ A))
56	54, 55	syl5ib 181	. 2 ⊢ (R Fr A → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → ¬ (xRy ∧ yRz ∧ zRx)))
57	56	imp 277	1 ⊢ ((R Fr A ∧ (x ∈ A ∧ y ∈ A ∧ z ∈ A)) → ¬ (xRy ∧ yRz ∧ zRx))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196   ∨ w3o 580   ∧ w3a 581   = weq 797  {cab 1090   = wceq 1091   ∈ wcel 1092  ∃wrex 1202   ∩ cin 1486   ⊆ wss 1487  ∅c0 1707  {ctp 1813   class class class wbr 2054   Fr wfr 2061

This theorem is referenced by:  epne3 2182  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-un 1076  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  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-tp 1814  df-op 1815  df-uni 1920  df-br 2063  df-fr 2169

metamath.org