Theorem ordwe 6326

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

Syntax hints:   → wi 4  Tr wtr 5202   E cep 5520   We wwe 5573  Ord word 6312

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 6316

This theorem is referenced by:  ordfr  6328  trssord  6330  tz7.5  6334  ordelord  6335  tz7.7  6339  oieu  9434  oiid  9436  hartogslem1  9437  oemapso  9581  cantnf  9592  oemapwe  9593  dfac8b  9931  fin23lem27  10228  om2uzoi  13866  ltweuz  13872  om2noseqoi  28236  wepwso  43163  onfrALTlem3  44664  onfrALTlem3VD  45006