Definition df-iord 4401

Description: Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively.

(Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4402 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-iord	⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-iord

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	word 4397	. 2 wff Ord 𝐴
3	1	wtr 4131	. . 3 wff Tr 𝐴
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1363	. . . . 5 class 𝑥
6	5	wtr 4131	. . . 4 wff Tr 𝑥
7	6, 4, 1	wral 2475	. . 3 wff ∀𝑥 ∈ 𝐴 Tr 𝑥
8	3, 7	wa 104	. 2 wff (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)
9	2, 8	wb 105	1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))

This definition is referenced by:  dford3  4402