Definition df-wetr 4431

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 4619). 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 4427	. 2 wff R We A
4	1, 2	wfr 4425	. . 3 wff R Fr A
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1396	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1396	. . . . . . . . 9 class y
9	6, 8, 2	wbr 4088	. . . . . . . 8 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1396	. . . . . . . . 9 class z
12	8, 11, 2	wbr 4088	. . . . . . . 8 wff y R z
13	9, 12	wa 104	. . . . . . 7 wff ( x R y /\ y R z )
14	6, 11, 2	wbr 4088	. . . . . . 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 2510	. . . . 5 wff A. z e. A ( ( x R y /\ y R z ) -> x R z )
17	16, 7, 1	wral 2510	. . . 4 wff A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
18	17, 5, 1	wral 2510	. . 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  4452  weeq1  4453  weeq2  4454  wefr  4455  wepo  4456  wetrep  4457  we0  4458  ordwe  4674  wessep  4676  reg3exmidlemwe  4677