Theorem dfwe2 6634

Description: Alternate definition of well-ordering. Definition 6.24(2) of [TakeutiZaring] p. 30. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)

Assertion

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

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

Proof of Theorem dfwe2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-we 4813	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
2		df-so 4774	. . . 4 |- ( R Or A <-> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
3		simpr 467	. . . . 5 |- ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) -> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) )
4		ax-1 6	. . . . . . . . . . . . . . 15 |- ( x R z -> ( ( x R y /\ y R z ) -> x R z ) )
5	4	a1i 11	. . . . . . . . . . . . . 14 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x R z -> ( ( x R y /\ y R z ) -> x R z ) ) )
6		fr2nr 4830	. . . . . . . . . . . . . . . . 17 |- ( ( R Fr A /\ ( x e. A /\ y e. A ) ) -> -. ( x R y /\ y R x ) )
7	6	3adantr3 1175	. . . . . . . . . . . . . . . 16 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( x R y /\ y R x ) )
8		breq2 4419	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( y R x <-> y R z ) )
9	8	anbi2d 715	. . . . . . . . . . . . . . . . 17 |- ( x = z -> ( ( x R y /\ y R x ) <-> ( x R y /\ y R z ) ) )
10	9	notbid 300	. . . . . . . . . . . . . . . 16 |- ( x = z -> ( -. ( x R y /\ y R x ) <-> -. ( x R y /\ y R z ) ) )
11	7, 10	syl5ibcom 228	. . . . . . . . . . . . . . 15 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x = z -> -. ( x R y /\ y R z ) ) )
12		pm2.21 112	. . . . . . . . . . . . . . 15 |- ( -. ( x R y /\ y R z ) -> ( ( x R y /\ y R z ) -> x R z ) )
13	11, 12	syl6 34	. . . . . . . . . . . . . 14 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x = z -> ( ( x R y /\ y R z ) -> x R z ) ) )
14		fr3nr 6632	. . . . . . . . . . . . . . . . 17 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( x R y /\ y R z /\ z R x ) )
15		df-3an 993	. . . . . . . . . . . . . . . . . . 19 |- ( ( x R y /\ y R z /\ z R x ) <-> ( ( x R y /\ y R z ) /\ z R x ) )
16	15	biimpri 211	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x R y /\ y R z ) /\ z R x ) -> ( x R y /\ y R z /\ z R x ) )
17	16	ancoms 459	. . . . . . . . . . . . . . . . 17 |- ( ( z R x /\ ( x R y /\ y R z ) ) -> ( x R y /\ y R z /\ z R x ) )
18	14, 17	nsyl 126	. . . . . . . . . . . . . . . 16 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( z R x /\ ( x R y /\ y R z ) ) )
19	18	pm2.21d 110	. . . . . . . . . . . . . . 15 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( z R x /\ ( x R y /\ y R z ) ) -> x R z ) )
20	19	expd 442	. . . . . . . . . . . . . 14 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( z R x -> ( ( x R y /\ y R z ) -> x R z ) ) )
21	5, 13, 20	3jaod 1341	. . . . . . . . . . . . 13 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R z \/ x = z \/ z R x ) -> ( ( x R y /\ y R z ) -> x R z ) ) )
22		frirr 4829	. . . . . . . . . . . . . 14 |- ( ( R Fr A /\ x e. A ) -> -. x R x )
23	22	3ad2antr1 1179	. . . . . . . . . . . . 13 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. x R x )
24	21, 23	jctild 550	. . . . . . . . . . . 12 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( ( x R z \/ x = z \/ z R x ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
25	24	ex 440	. . . . . . . . . . 11 |- ( R Fr A -> ( ( x e. A /\ y e. A /\ z e. A ) -> ( ( x R z \/ x = z \/ z R x ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) ) )
26	25	a2d 29	. . . . . . . . . 10 |- ( R Fr A -> ( ( ( x e. A /\ y e. A /\ z e. A ) -> ( x R z \/ x = z \/ z R x ) ) -> ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) ) )
27	26	alimdv 1773	. . . . . . . . 9 |- ( R Fr A -> ( A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( x R z \/ x = z \/ z R x ) ) -> A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) ) )
28	27	2alimdv 1775	. . . . . . . 8 |- ( R Fr A -> ( A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( x R z \/ x = z \/ z R x ) ) -> A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) ) )
29		r3al 2779	. . . . . . . 8 |- ( A. x e. A A. y e. A A. z e. A ( x R z \/ x = z \/ z R x ) <-> A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( x R z \/ x = z \/ z R x ) ) )
30		r3al 2779	. . . . . . . 8 |- ( A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) <-> A. x A. y A. z ( ( x e. A /\ y e. A /\ z e. A ) -> ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
31	28, 29, 30	3imtr4g 278	. . . . . . 7 |- ( R Fr A -> ( A. x e. A A. y e. A A. z e. A ( x R z \/ x = z \/ z R x ) -> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) ) )
32		ralidm 3884	. . . . . . . . 9 |- ( A. y e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A ( x R y \/ x = y \/ y R x ) )
33		breq2 4419	. . . . . . . . . . . 12 |- ( y = z -> ( x R y <-> x R z ) )
34		equequ2 1878	. . . . . . . . . . . 12 |- ( y = z -> ( x = y <-> x = z ) )
35		breq1 4418	. . . . . . . . . . . 12 |- ( y = z -> ( y R x <-> z R x ) )
36	33, 34, 35	3orbi123d 1347	. . . . . . . . . . 11 |- ( y = z -> ( ( x R y \/ x = y \/ y R x ) <-> ( x R z \/ x = z \/ z R x ) ) )
37	36	cbvralv 3030	. . . . . . . . . 10 |- ( A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. z e. A ( x R z \/ x = z \/ z R x ) )
38	37	ralbii 2830	. . . . . . . . 9 |- ( A. y e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A A. z e. A ( x R z \/ x = z \/ z R x ) )
39	32, 38	bitr3i 259	. . . . . . . 8 |- ( A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. y e. A A. z e. A ( x R z \/ x = z \/ z R x ) )
40	39	ralbii 2830	. . . . . . 7 |- ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) <-> A. x e. A A. y e. A A. z e. A ( x R z \/ x = z \/ z R x ) )
41		df-po 4773	. . . . . . 7 |- ( R Po A <-> A. x e. A A. y e. A A. z e. A ( -. x R x /\ ( ( x R y /\ y R z ) -> x R z ) ) )
42	31, 40, 41	3imtr4g 278	. . . . . 6 |- ( R Fr A -> ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> R Po A ) )
43	42	ancrd 561	. . . . 5 |- ( R Fr A -> ( A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) -> ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) ) )
44	3, 43	impbid2 209	. . . 4 |- ( R Fr A -> ( ( R Po A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) <-> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
45	2, 44	syl5bb 265	. . 3 |- ( R Fr A -> ( R Or A <-> A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
46	45	pm5.32i 647	. 2 |- ( ( R Fr A /\ R Or A ) <-> ( R Fr A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )
47	1, 46	bitri 257	1 |- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A ( x R y \/ x = y \/ y R x ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   \/ w3o 990   /\ w3a 991   A.wal 1452   e. wcel 1897   A.wral 2748   class class class wbr 4415   Po wpo 4771   Or wor 4772   Fr wfr 4808   We wwe 4810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-8 1899  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652  ax-un 6609

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-sbc 3279  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-tp 3984  df-op 3986  df-uni 4212  df-br 4416  df-po 4773  df-so 4774  df-fr 4811  df-we 4813

This theorem is referenced by:  ordon  6635  f1oweALT  6803  dford2  8150  fpwwe2lem12  9091  fpwwe2lem13  9092  dfon2  30486  fnwe2  35955