Theorem ordwe 6374

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 6364	. 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 5550   We wwe 5603  Ord word 6360

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 6364

This theorem is used by:  ordfr  6376  trssord  6378  tz7.5  6382  ordelord  6383  tz7.7  6387  oieu  9526  oiid  9528  hartogslem1  9529  oemapso  9676  cantnf  9687  oemapwe  9688  dfac8b  10103  fin23lem27  10399  om2uzoi  14091  ltweuz  14097  om2noseqoi  28682  wepwso  44029  onfrALTlem3  45512  onfrALTlem3VD  45854