Theorem ordwe 6370

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5212   E cep 5554   We wwe 5607  Ord word 6356

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ord 6360

This theorem is used by:  ordfr  6372  trssord  6374  tz7.5  6378  ordelord  6379  tz7.7  6383  oieu  9511  oiid  9513  hartogslem1  9514  oemapso  9661  cantnf  9672  oemapwe  9673  dfac8b  10034  fin23lem27  10330  om2uzoi  14019  ltweuz  14025  om2noseqoi  28568  wepwso  43884  onfrALTlem3  45367  onfrALTlem3VD  45709