Theorem ordtr 2952

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 2941	. 2 |- (Ord A <-> (Tr A /\ E We A))
2	1	pm3.26bi 322	1 |- (Ord A -> Tr A)

Syntax hints:   -> wi 3  Tr wtr 2670  Ecep 2819   We wwe 2906  Ord word 2937

This theorem is referenced by:  ordelss 2954  ordn2lp 2958  ordelord 2960  tz7.7 2963  ordelssne 2964  ordin 2967  onfr 2976  ssorduni 2983  onelsst 2990  ordtr1 2991  orduniss 3066  ordunisuc 3079  ontrc 3086  onuninsuc 3098  limsuc 3110  ordom 3131  elnn 3132

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 2941

Copyright terms: Public domain