Definition df-wetr 4071

Description: Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4247). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)

Assertion

Ref	Expression
df-wetr	|- ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )

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

Detailed syntax breakdown of Definition df-wetr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wwe 4067	. 2 wff R We A
4	1, 2	wfr 4065	. . 3 wff R Fr A
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1242	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1242	. . . . . . . . 9 class y
9	6, 8, 2	wbr 3764	. . . . . . . 8 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1242	. . . . . . . . 9 class z
12	8, 11, 2	wbr 3764	. . . . . . . 8 wff y R z
13	9, 12	wa 97	. . . . . . 7 wff ( x R y /\ y R z )
14	6, 11, 2	wbr 3764	. . . . . . 7 wff x R z
15	13, 14	wi 4	. . . . . 6 wff ( ( x R y /\ y R z ) -> x R z )
16	15, 10, 1	wral 2306	. . . . 5 wff A. z e. A ( ( x R y /\ y R z ) -> x R z )
17	16, 7, 1	wral 2306	. . . 4 wff A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
18	17, 5, 1	wral 2306	. . 3 wff A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
19	4, 18	wa 97	. 2 wff ( R Fr A /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) )
20	3, 19	wb 98	1 wff ( R We A <-> ( R Fr A /\ A. x e. A A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z ) ) )

This definition is referenced by:  nfwe  4092  weeq1  4093  weeq2  4094  wefr  4095  wepo  4096  wetrep  4097  we0  4098  ordwe  4300  wessep  4302  reg3exmidlemwe  4303