Theorem ordwe 6330

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

Syntax hints:   → wi 4  Tr wtr 5186   E cep 5524   We wwe 5577  Ord word 6316

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 208  df-an 397  df-ord 6320

This theorem is referenced by:  ordfr  6332  trssord  6334  tz7.5  6338  ordelord  6339  tz7.7  6343  oieu  9451  oiid  9453  hartogslem1  9454  oemapso  9601  cantnf  9612  oemapwe  9613  dfac8b  9951  fin23lem27  10248  om2uzoi  13915  ltweuz  13921  om2noseqoi  28320  wepwso  43495  onfrALTlem3  44995  onfrALTlem3VD  45337