Theorem ordtr 2213

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 2202	. 2 ⊢ (Ord A ↔ (Tr A ∧ E We A))
2	1	pm3.26bd 259	1 ⊢ (Ord A → Tr A)

Syntax hints:   → wi 2  Tr wtr 2041  Ecep 2056   We wwe 2062  Ord word 2198

This theorem is referenced by:  ordelss 2215  ordn2lp 2219  ordelord 2221  tz7.7 2224  ordelssne 2225  ordin 2228  onfr 2237  ssorduni 2249  onelsst 2255  ordtr1 2256  orduniss 2327  ordunisuc 2339  ontrc 2344  onuninsuc 2356  limsuc 2361  nlimsuc 2363  ordom 2382  elnn 2383

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ord 2202

metamath.org