Definition df-wetr 4457

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 do not have that as seen at ordtriexmid 4645). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition 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 4453	. 2 wff R We A
4	1, 2	wfr 4451	. . 3 wff R Fr A
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1397	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1397	. . . . . . . . 9 class y
9	6, 8, 2	wbr 4111	. . . . . . . 8 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1397	. . . . . . . . 9 class z
12	8, 11, 2	wbr 4111	. . . . . . . 8 wff y R z
13	9, 12	wa 104	. . . . . . 7 wff ( x R y /\ y R z )
14	6, 11, 2	wbr 4111	. . . . . . 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 2522	. . . . 5 wff A. z e. A ( ( x R y /\ y R z ) -> x R z )
17	16, 7, 1	wral 2522	. . . 4 wff A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
18	17, 5, 1	wral 2522	. . 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 104	. 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 105	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  4478  weeq1  4479  weeq2  4480  wefr  4481  wepo  4482  wetrep  4483  we0  4484  ordwe  4700  wessep  4702  reg3exmidlemwe  4703