Definition df-iord 4103

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". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4104 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 4099	. 2 wff Ord 𝐴
3	1	wtr 3854	. . 3 wff Tr 𝐴
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1242	. . . . 5 class 𝑥
6	5	wtr 3854	. . . 4 wff Tr 𝑥
7	6, 4, 1	wral 2306	. . 3 wff ∀𝑥 ∈ 𝐴 Tr 𝑥
8	3, 7	wa 97	. 2 wff (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)
9	2, 8	wb 98	1 wff (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥))

This definition is referenced by:  dford3  4104