Theorem ordwe 6370

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

Syntax hints:   → wi 4  Tr wtr 5219   E cep 5558   We wwe 5611  Ord word 6356

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 210  df-an 401  df-ord 6360

This theorem is referenced by:  ordfr  6372  trssord  6374  tz7.5  6378  ordelord  6379  tz7.7  6383  oieu  9497  oiid  9499  hartogslem1  9500  oemapso  9647  cantnf  9658  oemapwe  9659  dfac8b  10011  fin23lem27  10308  om2uzoi  13987  ltweuz  13993  om2noseqoi  28458  wepwso  43655  onfrALTlem3  45138  onfrALTlem3VD  45480