Theorem dfwe2 2187

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 group(s):   x,y,R   x,A,y

Proof of Theorem dfwe2

Step	Hyp	Ref	Expression
1		df-we 2186	. 2 |- (R We A <-> (R Fr A /\ R Or A))
2		solin 2145	. . . . . . 7 |- ((R Or A /\ (x e. A /\ y e. A)) -> (xRy \/ x = y \/ yRx))
3	2	exp 291	. . . . . 6 |- (R Or A -> ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
4	3	19.21aivv 944	. . . . 5 |- (R Or A -> A.xA.y((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
5		r2al 1231	. . . . 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 175	. . . 4 |- (R Or A -> A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
7	6	anim2i 270	. . 3 |- ((R Fr A /\ R Or A) -> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
8		frirr 2176	. . . . . . . . . . . . . . . . 17 |- ((R Fr A /\ x e. A) -> -. xRx)
9	8	adantrr 312	. . . . . . . . . . . . . . . 16 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. xRx)
10		3simpa 591	. . . . . . . . . . . . . . . 16 |- ((x e. A /\ y e. A /\ z e. A) -> (x e. A /\ y e. A))
11	9, 10	sylan2 346	. . . . . . . . . . . . . . 15 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. xRx)
12	11	a1d 14	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> -. xRx))
13		fr2nr 2177	. . . . . . . . . . . . . . . . . . . . 21 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))
14	13, 10	sylan2 346	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRx))
15		breq2 2066	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = z -> (yRx <-> yRz))
16	15	biimprd 136	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = z -> (yRz -> yRx))
17	16	anim2d 433	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> ((xRy /\ yRz) -> (xRy /\ yRx)))
18	17	com12 13	. . . . . . . . . . . . . . . . . . . . 21 |- ((xRy /\ yRz) -> (x = z -> (xRy /\ yRx)))
19	18	imp 277	. . . . . . . . . . . . . . . . . . . 20 |- (((xRy /\ yRz) /\ x = z) -> (xRy /\ yRx))
20	14, 19	nsyl 102	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ x = z))
21		imnan 207	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. x = z) <-> -. ((xRy /\ yRz) /\ x = z))
22	20, 21	sylibr 175	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. x = z))
23		fr3nr 2178	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
24		df-3an 583	. . . . . . . . . . . . . . . . . . . . 21 |- ((xRy /\ yRz /\ zRx) <-> ((xRy /\ yRz) /\ zRx))
25	24	negbii 162	. . . . . . . . . . . . . . . . . . . 20 |- (-. (xRy /\ yRz /\ zRx) <-> -. ((xRy /\ yRz) /\ zRx))
26	23, 25	sylib 173	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ zRx))
27		imnan 207	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. zRx) <-> -. ((xRy /\ yRz) /\ zRx))
28	26, 27	sylibr 175	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. zRx))
29	22, 28	jcad 455	. . . . . . . . . . . . . . . . 17 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> (-. x = z /\ -. zRx)))
30		ioran 254	. . . . . . . . . . . . . . . . 17 |- (-. (x = z \/ zRx) <-> (-. x = z /\ -. zRx))
31	29, 30	syl6ibr 186	. . . . . . . . . . . . . . . 16 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. (x = z \/ zRx)))
32	31	syl4d 28	. . . . . . . . . . . . . . 15 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((-. (x = z \/ zRx) -> xRz) -> ((xRy /\ yRz) -> xRz)))
33		3orass 584	. . . . . . . . . . . . . . . 16 |- ((xRz \/ x = z \/ zRx) <-> (xRz \/ (x = z \/ zRx)))
34		orcom 209	. . . . . . . . . . . . . . . 16 |- ((xRz \/ (x = z \/ zRx)) <-> ((x = z \/ zRx) \/ xRz))
35		df-or 197	. . . . . . . . . . . . . . . 16 |- (((x = z \/ zRx) \/ xRz) <-> (-. (x = z \/ zRx) -> xRz))
36	33, 34, 35	3bitr 155	. . . . . . . . . . . . . . 15 |- ((xRz \/ x = z \/ zRx) <-> (-. (x = z \/ zRx) -> xRz))
37	32, 36	syl5ib 181	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> ((xRy /\ yRz) -> xRz)))
38	12, 37	jcad 455	. . . . . . . . . . . . 13 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> (-. xRx /\ ((xRy /\ yRz) -> xRz))))
39	38	exp 291	. . . . . . . . . . . 12 |- (R Fr A -> ((x e. A /\ y e. A /\ z e. A) -> ((xRz \/ x = z \/ zRx) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))))
40	39	a2d 15	. . . . . . . . . . 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)))))
41	40	19.20dv 946	. . . . . . . . . 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)))))
42	41	19.20dv 946	. . . . . . . . 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)))))
43	42	19.20dv 946	. . . . . . . 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)))))
44		r3al 1240	. . . . . . . 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)))
45		r3al 1240	. . . . . . . 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))))
46	43, 44, 45	3imtr4g 426	. . . . . . 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))))
47		ralidm 1774	. . . . . . . . 9 |- (A.y e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A (xRy \/ x = y \/ yRx))
48		breq2 2066	. . . . . . . . . . . 12 |- (y = z -> (xRy <-> xRz))
49		cleq2 1110	. . . . . . . . . . . 12 |- (y = z -> (x = y <-> x = z))
50		breq1 2065	. . . . . . . . . . . 12 |- (y = z -> (yRx <-> zRx))
51	48, 49, 50	bi3ord 635	. . . . . . . . . . 11 |- (y = z -> ((xRy \/ x = y \/ yRx) <-> (xRz \/ x = z \/ zRx)))
52	51	cbvralv 1333	. . . . . . . . . 10 |- (A.y e. A (xRy \/ x = y \/ yRx) <->