Theorem dfwe2 2925

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 2924	. 2 |- (R We A <-> (R Fr A /\ R Or A))
2		solin 2848	. . . . . . 7 |- ((R Or A /\ (x e. A /\ y e. A)) -> (xRy \/ x = y \/ yRx))
3	2	ex 373	. . . . . 6 |- (R Or A -> ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
4	3	19.21aivv 1282	. . . . 5 |- (R Or A -> A.xA.y((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx)))
5		r2al 1668	. . . . 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 200	. . . 4 |- (R Or A -> A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
7	6	anim2i 335	. . 3 |- ((R Fr A /\ R Or A) -> (R Fr A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
8		fr2nr 2915	. . . . . . . . . . . . . . . . . . . . 21 |- ((R Fr A /\ (x e. A /\ y e. A)) -> -. (xRy /\ yRx))
9	8	3adantr3 806	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRx))
10		breq2 2613	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = z -> (yRx <-> yRz))
11	10	biimprd 154	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = z -> (yRz -> yRx))
12	11	anim2d 559	. . . . . . . . . . . . . . . . . . . . 21 |- (x = z -> ((xRy /\ yRz) -> (xRy /\ yRx)))
13	12	impcom 351	. . . . . . . . . . . . . . . . . . . 20 |- (((xRy /\ yRz) /\ x = z) -> (xRy /\ yRx))
14	9, 13	nsyl 116	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ x = z))
15		imnan 242	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. x = z) <-> -. ((xRy /\ yRz) /\ x = z))
16	14, 15	sylibr 200	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. x = z))
17		fr3nr 2916	. . . . . . . . . . . . . . . . . . . 20 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. (xRy /\ yRz /\ zRx))
18		df-3an 775	. . . . . . . . . . . . . . . . . . . . 21 |- ((xRy /\ yRz /\ zRx) <-> ((xRy /\ yRz) /\ zRx))
19	18	negbii 187	. . . . . . . . . . . . . . . . . . . 20 |- (-. (xRy /\ yRz /\ zRx) <-> -. ((xRy /\ yRz) /\ zRx))
20	17, 19	sylib 198	. . . . . . . . . . . . . . . . . . 19 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. ((xRy /\ yRz) /\ zRx))
21		imnan 242	. . . . . . . . . . . . . . . . . . 19 |- (((xRy /\ yRz) -> -. zRx) <-> -. ((xRy /\ yRz) /\ zRx))
22	20, 21	sylibr 200	. . . . . . . . . . . . . . . . . 18 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> -. zRx))
23	16, 22	jcad 598	. . . . . . . . . . . . . . . . 17 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRy /\ yRz) -> (-. x = z /\ -. zRx)))
24		ioran 306	. . . . . . . . . . . . . . . . 17 |- (-. (x = z \/ zRx) <-> (-. x = z /\ -. zRx))
25	23, 24	syl6ibr 213	. . . . . . . . . . . . . . . 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 776	. . . . . . . . . . . . . . . 16 |- ((xRz \/ x = z \/ zRx) <-> (xRz \/ (x = z \/ zRx)))
28		orcom 246	. . . . . . . . . . . . . . . 16 |- ((xRz \/ (x = z \/ zRx)) <-> ((x = z \/ zRx) \/ xRz))
29		df-or 224	. . . . . . . . . . . . . . . 16 |- (((x = z \/ zRx) \/ xRz) <-> (-. (x = z \/ zRx) -> xRz))
30	27, 28, 29	3bitr 177	. . . . . . . . . . . . . . 15 |- ((xRz \/ x = z \/ zRx) <-> (-. (x = z \/ zRx) -> xRz))
31	26, 30	syl5ib 206	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> ((xRy /\ yRz) -> xRz)))
32		frirr 2914	. . . . . . . . . . . . . . 15 |- ((R Fr A /\ x e. A) -> -. xRx)
33	32	3ad2antr1 810	. . . . . . . . . . . . . 14 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> -. xRx)
34	31, 33	jctild 599	. . . . . . . . . . . . 13 |- ((R Fr A /\ (x e. A /\ y e. A /\ z e. A)) -> ((xRz \/ x = z \/ zRx) -> (-. xRx /\ ((xRy /\ yRz) -> xRz))))
35	34	ex 373	. . . . . . . . . . . 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 1284	. . . . . . . . . 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 1284	. . . . . . . . 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 1284	. . . . . . . 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 1682	. . . . . . . 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 1682	. . . . . . . 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 551	. . . . . . 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 2347	. . . . . . . . 9 |- (A.y e. A A.y e. A (xRy \/ x = y \/ yRx) <-> A.y e. A (xRy \/ x = y \/ yRx))
44		breq2 2613	. . . . . . . . . . . 12 |- (y = z -> (xRy <-> xRz))
45		eqeq2 1476	. . . . . . . . . . . 12 |- (y = z -> (x = y <-> x = z))
46		breq1 2612	. . . . . . . . . . . 12 |- (y = z -> (yRx <-> zRx))
47	44, 45, 46	3orbi123d 889	. . . . . . . . . . 11 |- (y = z -> ((xRy \/ x = y \/ yRx) <-> (xRz \/ x = z \/ zRx)))
48	47	cbvralv 1791	. . . . . . . . . 10 |- (A.y e. A (xRy \/ x = y \/ yRx) <-> A.z e. A (xRz \/ x = z \/ zRx))
49	48	ralbii 1659	. . . . . . . . 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	bitr3 175	. . . . . . . 8 |- (