Theorem ontrci 3915

Description: An ordinal number is a transitive class.

Hypothesis

Ref	Expression
on.1	|- A e. On

Assertion

Ref	Expression
ontrci	|- Tr A

Proof of Theorem ontrci

Step	Hyp	Ref	Expression
1		on.1	. . 3 |- A e. On
2	1	onordi 3914	. 2 |- Ord A
3		ordtr 3825	. 2 |- (Ord A -> Tr A)
4	2, 3	ax-mp 7	1 |- Tr A

Syntax hints:   e. wcel 1588  Tr wtr 3579  Ord word 3810  Oncon0 3811

This theorem is referenced by:  onunisuci 3923

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-ral 2359  df-rex 2360  df-v 2540  df-in 2834  df-ss 2836  df-uni 3367  df-tr 3580  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815

Copyright terms: Public domain