Theorem ordwe 6353

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 6343	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simprbi 501	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5204   E cep 5542   We wwe 5595  Ord word 6339

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 209  df-an 400  df-ord 6343

This theorem is referenced by:  ordfr  6355  trssord  6357  tz7.5  6361  ordelord  6362  tz7.7  6366  oieu  9480  oiid  9482  hartogslem1  9483  oemapso  9630  cantnf  9641  oemapwe  9642  dfac8b  9980  fin23lem27  10278  om2uzoi  13961  ltweuz  13967  om2noseqoi  28383  wepwso  43580  onfrALTlem3  45080  onfrALTlem3VD  45422