Theorem ordwe 6410

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

Syntax hints:   → wi 4  Tr wtr 5283   E cep 5598   We wwe 5651  Ord word 6396

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 6400

This theorem is referenced by:  ordfr  6412  trssord  6414  tz7.5  6418  ordelord  6419  tz7.7  6423  oieu  9610  oiid  9612  hartogslem1  9613  oemapso  9753  cantnf  9764  oemapwe  9765  dfac8b  10102  fin23lem27  10399  om2uzoi  14008  ltweuz  14014  om2noseqoi  28329  wepwso  43002  onfrALTlem3  44517  onfrALTlem3VD  44860