Theorem dfwe2 3140

Description: Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30.

Assertion

Ref	Expression
dfwe2	|- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))

Distinct variable groups:   x,y,R   x,A,y

Proof of Theorem dfwe2

Step	Hyp	Ref	Expression
1		df-we 2962	. 2 |- (R We A <-> (R Fr A /\ R Or A))
2		solin 2936	. . . . . . 7 |- ((R Or A /\ (x e. A /\ y e. A)) -> (xRy \/ x = y \/ yRx))
3	2	ex 371	. . . . . 6 |- (R Or A -> ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
4	3	19.21aivv 1325	. . . . 5 |- (R Or A -> A.xA.y((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
5		r2al 1722	. . . . 5 |- (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.xA.y((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
6	4, 5	sylibr 198	. . . 4 |- (R Or A -> A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
7	6	anim2i 333	. . 3 |- ((R Fr A /\ R Or A) -> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
8		fr2nr 2955	. . . . . . . . . . . . . . . . . . . . 21 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))
9	8	3adantr3 814	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRx))
10		breq2 2696	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = z -> (yRx <-> yRz))
11	10	biimprd 152	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> (yRz -> yRx))
12	11	anim2d 564	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> ((xRy /\ yRz) -> (xRy /\ yRx)))
13	12	impcom 349	. . . . . . . . . . . . . . . . . . . 20 |- (((xRy /\ yRz) /\ x = z) -> (xRy /\ yRx))
14	9, 13	nsyl 115	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ x = z))
15		imnan 240	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. x = z) <-> -. ((xRy /\ yRz) /\ x = z))
16	14, 15	sylibr 198	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. x = z))
17		fr3nr 3138	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
18		df-3an 783	. . . . . . . . . . . . . . . . . . . . 21 |- ((xRy /\ yRz /\ zRx) <-> ((xRy /\ yRz) /\ zRx))
19	18	notbii 185	. . . . . . . . . . . . . . . . . . . 20 |- (-. (xRy /\ yRz /\ zRx) <-> -. ((xRy /\ yRz) /\ zRx))
20	17, 19	sylib 196	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ zRx))
21		imnan 240	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. zRx) <-> -. ((xRy /\ yRz) /\ zRx))
22	20, 21	sylibr 198	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. zRx))
23	16, 22	jcad 603	. . . . . . . . . . . . . . . . 17 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> (-. x = z /\ -. zRx)))
24		ioran 304	. . . . . . . . . . . . . . . . 17 |- (-. (x = z \/ zRx) <-> (-. x = z /\ -. zRx))
25	23, 24	syl6ibr 211	. . . . . . . . . . . . . . . 16 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. (x = z \/ zRx)))
26	25	imim1d 28	. . . . . . . . . . . . . . 15 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((-. (x = z \/ zRx) -> xRz) -> ((xRy /\ yRz) -> xRz)))
27		3orass 784	. . . . . . . . . . . . . . . 16 |- ((xRz \/ x = z \/ zRx) <-> (xRz \/ (x = z \/ zRx)))
28		orcom 244	. . . . . . . . . . . . . . . 16 |- ((xRz \/ (x = z \/ zRx)) <-> ((x = z \/ zRx) \/ xRz))
29		df-or 222	. . . . . . . . . . . . . . . 16 |- (((x = z \/ zRx) \/ xRz) <-> (-. (x = z \/ zRx) -> xRz))
30	27, 28, 29	3bitri 175	. . . . . . . . . . . . . . 15 |- ((xRz \/ x = z \/ zRx) <-> (-. (x = z \/ zRx) -> xRz))
31	26, 30	syl5ib 204	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> ((xRy /\ yRz) -> xRz)))
32		frirr 2954	. . . . . . . . . . . . . . 15 |- ((R Fr A /\ x e. A) -> -. xRx)
33	32	3ad2antr1 818	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. xRx)
34	31, 33	jctild 604	. . . . . . . . . . . . 13 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> (-. xRx /\ ((xRy /\ yRz) -> xRz))))
35	34	ex 371	. . . . . . . . . . . 12 |- (R Fr A -> ((x e. A /\ y e. A /\ z e. A) -> ((xRz \/ x = z \/ zRx) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
36	35	a2d 13	. . . . . . . . . . 11 |- (R Fr A -> (((x e. A /\ y e. A /\ z e. A) -> (xRz \/ x = z \/ zRx)) -> ((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
37	36	19.20dv 1327	. . . . . . . . . 10 |- (R Fr A -> (A.z((x e. A /\ y e. A /\ z e. A) -> (xRz \/ x = z \/ zRx)) -> A.z((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
38	37	19.20dv 1327	. . . . . . . . 9 |- (R Fr A -> (A.yA.z((x e. A /\ y e. A /\ z e. A) -> (xRz \/ x = z \/ zRx)) -> A.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
39	38	19.20dv 1327	. . . . . . . 8 |- (R Fr A -> (A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (xRz \/ x = z \/ zRx)) -> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
40		r3al 1736	. . . . . . . 8 |- (A.x e. A A.y e. A A.z e. A (xRz \/ x = z \/ zRx) <-> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (xRz \/ x = z \/ zRx)))
41		r3al 1736	. . . . . . . 8 |- (A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)) <-> A.xA.yA.z((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz))))
42	39, 40, 41	3imtr4g 556	. . . . . . 7 |- (R Fr A -> (A.x e. A A.y e. A A.z e. A (xRz \/ x = z \/ zRx) -> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz))))
43		ralidm 2411	. . . . . . . . 9 |- (A.y e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A (xRy \/ x = y \/ yRx))
44		breq2 2696	. . . . . . . . . . . 12 |- (y = z -> (xRy <-> xRz))
45		eqeq2 1527	. . . . . . . . . . . 12 |- (y = z -> (x = y <-> x = z))
46		breq1 2695	. . . . . . . . . . . 12 |- (y = z -> (yRx <-> zRx))
47	44, 45, 46	3orbi123d 898	. . . . . . . . . . 11 |- (y = z -> ((xRy \/ x = y \/ yRx) <-> (xRz \/ x = z \/ zRx)))
48	47	cbvralv 1846	. . . . . . . . . 10 |- (A.y e. A (xRy \/ x = y \/ yRx) <-> A.z e. A (xRz \/ x = z \/ zRx))
49	48	ralbii 1713	. . . . . . . . 9 |- (A.y e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A A.z e. A (xRz \/ x = z \/ zRx))
50	43, 49	bitr3i 173	. . . . . . . 8 |- (A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A A.z e. A (xRz \/ x = z \/ zRx))
51	50	ralbii 1713	. . . . . . 7 |- (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.x e. A A.y e. A A.z e. A (xRz \/ x = z \/ zRx))
52		df-po 2918	. . . . . . 7 |- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
53	42, 51, 52	3imtr4g 556	. . . . . 6 |- (R Fr A -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) -> R Po A))
54	53	ancrd 297	. . . . 5 |- (R Fr A -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) -> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))))
55		df-so 2929	. . . . 5 |- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
56	54, 55	syl6ibr 211	. . . 4 |- (R Fr A -> (A.x e. A A.y e. A (xRy \/ x = y \/ yRx) -> R Or A))
57	56	imdistani 445	. . 3 |- ((R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)) -> (R Fr A /\ R Or A))
58	7, 57	impbii 155	. 2 |- ((R Fr A /\ R Or A) <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
59	1, 58	bitri 171	1 |- (R We A <-> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 144   \/ wo 220   /\ wa 221   \/ w3o 780   /\ w3a 781  A.wal 990   = wceq 992   e. wcel 994  A.wral 1691   class class class wbr 2692   Po wpo 2916   Or wor 2917   Fr wfr 2945   We wwe 2946

This theorem is referenced by:  ordon 3141  weinxp 3319  isowe 4017  f1oweALT 4020

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 782  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-tp 2473  df-op 2474  df-uni 2570  df-br 2693  df-po 2918  df-so 2929  df-fr 2947  df-we 2962

Copyright terms: Public domain