Definition df-wetr 4328

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 4514). 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	⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧

Detailed syntax breakdown of Definition df-wetr

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wwe 4324	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 4322	. . 3 wff 𝑅 Fr 𝐴
5		vx	. . . . . . . . . 10 setvar 𝑥
6	5	cv 1352	. . . . . . . . 9 class 𝑥
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1352	. . . . . . . . 9 class 𝑦
9	6, 8, 2	wbr 3998	. . . . . . . 8 wff 𝑥𝑅𝑦
10		vz	. . . . . . . . . 10 setvar 𝑧
11	10	cv 1352	. . . . . . . . 9 class 𝑧
12	8, 11, 2	wbr 3998	. . . . . . . 8 wff 𝑦𝑅𝑧
13	9, 12	wa 104	. . . . . . 7 wff (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)
14	6, 11, 2	wbr 3998	. . . . . . 7 wff 𝑥𝑅𝑧
15	13, 14	wi 4	. . . . . 6 wff ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
16	15, 10, 1	wral 2453	. . . . 5 wff ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
17	16, 7, 1	wral 2453	. . . 4 wff ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
18	17, 5, 1	wral 2453	. . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)
19	4, 18	wa 104	. 2 wff (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))
20	3, 19	wb 105	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

This definition is referenced by:  nfwe  4349  weeq1  4350  weeq2  4351  wefr  4352  wepo  4353  wetrep  4354  we0  4355  ordwe  4569  wessep  4571  reg3exmidlemwe  4572