Theorem ordwe 6366

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

Syntax hints:   → wi 4  Tr wtr 5258   E cep 5572   We wwe 5623  Ord word 6352

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 397  df-ord 6356

This theorem is referenced by:  ordfr  6368  trssord  6370  tz7.5  6374  ordelord  6375  tz7.7  6379  oieu  9516  oiid  9518  hartogslem1  9519  oemapso  9659  cantnf  9670  oemapwe  9671  dfac8b  10008  fin23lem27  10305  om2uzoi  13902  ltweuz  13908  wepwso  41554  onfrALTlem3  43074  onfrALTlem3VD  43417