Theorem ontrci

Description: An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994)

	Ref	Expression
Hypothesis	on.1	⊢ 𝐴 ∈ On
Assertion	ontrci	⊢ Tr 𝐴

Proof

Step	Hyp	Ref	Expression
1		on.1	⊢ 𝐴 ∈ On
2	1	onordi	⊢ Ord 𝐴
3		ordtr	⊢ ( Ord 𝐴 → Tr 𝐴 )
4	2 3	ax-mp	⊢ Tr 𝐴