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 497	1 ⊢ (Ord 𝐴 → E We 𝐴)

Syntax hints:   → wi 4  Tr wtr 5193   E cep 5523   We wwe 5576  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 207  df-an 396  df-ord 6320

This theorem is referenced by:  ordfr  6332  trssord  6334  tz7.5  6338  ordelord  6339  tz7.7  6343  oieu  9447  oiid  9449  hartogslem1  9450  oemapso  9594  cantnf  9605  oemapwe  9606  dfac8b  9944  fin23lem27  10241  om2uzoi  13908  ltweuz  13914  om2noseqoi  28309  wepwso  43489  onfrALTlem3  44989  onfrALTlem3VD  45331