Definition df-wetr 4333

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 4519). 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 4329	. 2 wff R We A
4	1, 2	wfr 4327	. . 3 wff R Fr A
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1352	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1352	. . . . . . . . 9 class y
9	6, 8, 2	wbr 4002	. . . . . . . 8 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1352	. . . . . . . . 9 class z
12	8, 11, 2	wbr 4002	. . . . . . . 8 wff y R z
13	9, 12	wa 104	. . . . . . 7 wff ( x R y /\ y R z )
14	6, 11, 2	wbr 4002	. . . . . . 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 2455	. . . . 5 wff A. z e. A ( ( x R y /\ y R z ) -> x R z )
17	16, 7, 1	wral 2455	. . . 4 wff A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
18	17, 5, 1	wral 2455	. . 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  4354  weeq1  4355  weeq2  4356  wefr  4357  wepo  4358  wetrep  4359  we0  4360  ordwe  4574  wessep  4576  reg3exmidlemwe  4577