Definition df-iord 4048

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 4049 instead for naming consistency with set.mm. (New usage is discouraged.)

Assertion

Ref	Expression
df-iord	⊢ (Ord A ↔ (Tr A ∧ ∀x ∈ A Tr x))

Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-iord

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	word 4044	. 2 wff Ord A
3	1	wtr 3824	. . 3 wff Tr A
4		vx	. . . . . 6 setvar x
5	4	cv 1225	. . . . 5 class x
6	5	wtr 3824	. . . 4 wff Tr x
7	6, 4, 1	wral 2280	. . 3 wff ∀x ∈ A Tr x
8	3, 7	wa 97	. 2 wff (Tr A ∧ ∀x ∈ A Tr x)
9	2, 8	wb 98	1 wff (Ord A ↔ (Tr A ∧ ∀x ∈ A Tr x))

This definition is referenced by:  dford3  4049