Theorem ordwe 6182

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

Syntax hints:   → wi 4  Tr wtr 5138   E cep 5434   We wwe 5482  Ord word 6168

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 400  df-ord 6172

This theorem is referenced by:  ordfr  6184  trssord  6186  tz7.5  6190  ordelord  6191  tz7.7  6195  oieu  9036  oiid  9038  hartogslem1  9039  oemapso  9178  cantnf  9189  oemapwe  9190  dfac8b  9491  fin23lem27  9788  om2uzoi  13372  ltweuz  13378  wepwso  40360  onfrALTlem3  41623  onfrALTlem3VD  41966