Theorem ordwe 6264

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

Syntax hints:   → wi 4  Tr wtr 5187   E cep 5485   We wwe 5534  Ord word 6250

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 396  df-ord 6254

This theorem is referenced by:  ordfr  6266  trssord  6268  tz7.5  6272  ordelord  6273  tz7.7  6277  oieu  9228  oiid  9230  hartogslem1  9231  oemapso  9370  cantnf  9381  oemapwe  9382  dfac8b  9718  fin23lem27  10015  om2uzoi  13603  ltweuz  13609  wepwso  40784  onfrALTlem3  42053  onfrALTlem3VD  42396