Theorem ordtr 2962

Description: An ordinal class is transitive.

Assertion

Ref	Expression
ordtr	|- (Ord A -> Tr A)

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 2951	. 2 |- (Ord A <-> (Tr A /\ E We A))
2	1	pm3.26bi 322	1 |- (Ord A -> Tr A)

Syntax hints:   -> wi 3  Tr wtr 2680  Ecep 2830   We wwe 2916  Ord word 2947

This theorem is referenced by:  ordelss 2964  ordn2lp 2968  ordelord 2970  tz7.7 2973  ordelssne 2974  ordin 2977  onfr 2986  ssorduni 2993  onelsst 3000  ordtr1 3001  orduniss 3076  ordunisuc 3089  ontrc 3096  onuninsuc 3108  limsuc 3120  ordom 3141  elnn 3142

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-ord 2951

Copyright terms: Public domain