Theorem ordwe 6279

Description: Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordwe	⊢ (Ord 𝐴 → E We 𝐴)

Proof of Theorem ordwe

Step	Hyp	Ref	Expression
1		df-ord 6269	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 497	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5191   E cep 5494   We wwe 5543  Ord word 6265

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ord 6269

This theorem is referenced by:  ordfr  6281  trssord  6283  tz7.5  6287  ordelord  6288  tz7.7  6292  oieu  9298  oiid  9300  hartogslem1  9301  oemapso  9440  cantnf  9451  oemapwe  9452  dfac8b  9787  fin23lem27  10084  om2uzoi  13675  ltweuz  13681  wepwso  40868  onfrALTlem3  42164  onfrALTlem3VD  42507