Definition df-wetr 4479

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 4668). 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 4475	. 2 wff R We A
4	1, 2	wfr 4473	. . 3 wff R Fr A
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1401	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1401	. . . . . . . . 9 class y
9	6, 8, 2	wbr 4130	. . . . . . . 8 wff x R y
10		vz	. . . . . . . . . 10 setvar z
11	10	cv 1401	. . . . . . . . 9 class z
12	8, 11, 2	wbr 4130	. . . . . . . 8 wff y R z
13	9, 12	wa 104	. . . . . . 7 wff ( x R y /\ y R z )
14	6, 11, 2	wbr 4130	. . . . . . 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 2528	. . . . 5 wff A. z e. A ( ( x R y /\ y R z ) -> x R z )
17	16, 7, 1	wral 2528	. . . 4 wff A. y e. A A. z e. A ( ( x R y /\ y R z ) -> x R z )
18	17, 5, 1	wral 2528	. . 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 used by:  nfwe  4500  weeq1  4501  weeq2  4502  wefr  4503  wepo  4504  wetrep  4505  we0  4506  ordwe  4723  wessep  4725  reg3exmidlemwe  4726