Theorem ordwe 6319

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

Syntax hints:   → wi 4  Tr wtr 5198   E cep 5515   We wwe 5568  Ord word 6305

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 207  df-an 396  df-ord 6309

This theorem is referenced by:  ordfr  6321  trssord  6323  tz7.5  6327  ordelord  6328  tz7.7  6332  oieu  9425  oiid  9427  hartogslem1  9428  oemapso  9572  cantnf  9583  oemapwe  9584  dfac8b  9922  fin23lem27  10219  om2uzoi  13862  ltweuz  13868  om2noseqoi  28234  wepwso  43082  onfrALTlem3  44583  onfrALTlem3VD  44925