Theorem dfwe2 6623

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 4814	. 2 |- ( R We A <-> ( R Fr A /\ R Or A ) )
2		df-so 4775	. . . 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 462	. . . . 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 4831	. . . . . . . . . . . . . . . . 17 |- ( ( R Fr A /\ ( x e. A /\ y e. A ) ) -> -. ( x R y /\ y R x ) )
7	6	3adantr3 1166	. . . . . . . . . . . . . . . 16 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. ( x R y /\ y R x ) )
8		breq2 4427	. . . . . . . . . . . . . . . . . 18 |- ( x = z -> ( y R x <-> y R z ) )
9	8	anbi2d 708	. . . . . . . . . . . . . . . . 17 |- ( x = z -> ( ( x R y /\ y R x ) <-> ( x R y /\ y R z ) ) )
10	9	notbid 295	. . . . . . . . . . . . . . . 16 |- ( x = z -> ( -. ( x R y /\ y R x ) <-> -. ( x R y /\ y R z ) ) )
11	7, 10	syl5ibcom 223	. . . . . . . . . . . . . . 15 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> ( x = z -> -. ( x R y /\ y R z ) ) )
12		pm2.21 111	. . . . . . . . . . . . . . 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 6621	. . . . . . . . . . . . . . . . 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 984	. . . . . . . . . . . . . . . . . . 19 |- ( ( x R y /\ y R z /\ z R x ) <-> ( ( x R y /\ y R z ) /\ z R x ) )
16	15	biimpri 209	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x R y /\ y R z ) /\ z R x ) -> ( x R y /\ y R z /\ z R x ) )
17	16	ancoms 454	. . . . . . . . . . . . . . . . 17 |- ( ( z R x /\ ( x R y /\ y R z ) ) -> ( x R y /\ y R z /\ z R x ) )
18	14, 17	nsyl 124	. . . . . . . . . . . . . . . 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 109	. . . . . . . . . . . . . . 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 437	. . . . . . . . . . . . . 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 1328	. . . . . . . . . . . . 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 4830	. . . . . . . . . . . . . 14 |- ( ( R Fr A /\ x e. A ) -> -. x R x )
23	22	3ad2antr1 1170	. . . . . . . . . . . . 13 |- ( ( R Fr A /\ ( x e. A /\ y e. A /\ z e. A ) ) -> -. x R x )
24	21, 23	jctild 545	. . . . . . . . . . . 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 435	. . . . . . . . . . 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 1757	. . . . . . . . 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 1759	. . . . . . . 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 2802	. . . . . . . 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 2802	. . . . . . . 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 273	. . . . . . 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 3903	. . . . . . . . 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 4427	. . . . . . . . . . . 12 |- ( y = z -> ( x R y <-> x R z ) )
34		equequ2 1853	. . . . . . . . . . . 12 |- ( y = z -> ( x = y <-> x = z ) )
35		breq1 4426	. . . . . . . . . . . 12 |- ( y = z -> ( y R x <-> z R x ) )
36	33, 34, 35	3orbi123d 1334	. . . . . . . . . . 11 |- ( y = z -> ( ( x R y \/ x = y \/ y R x ) <-> ( x R z \/ x = z \/ z R x ) ) )
37	36	cbvralv 3054	. . . . . . . . . 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 2853	. . . . . . . . 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 254	. . . . . . . 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 2853	. . . . . . 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 4774	. . . . . . 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 273	. . . . . 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 556	. . . . 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 207	. . . 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 260	. . 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 641	. 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 252	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 187   /\ wa 370   \/ w3o 981   /\ w3a 982   A.wal 1435   e. wcel 1872   A.wral 2771   class class class wbr 4423   Po wpo 4772   Or wor 4773   Fr wfr 4809   We wwe 4811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6598

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-po 4774  df-so 4775  df-fr 4812  df-we 4814

This theorem is referenced by:  ordon  6624  f1oweALT  6792  dford2  8135  fpwwe2lem12  9074  fpwwe2lem13  9075  dfon2  30446  fnwe2  35882