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

Syntax hints:   → wi 4  Tr wtr 5205   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  9444  oiid  9446  hartogslem1  9447  oemapso  9591  cantnf  9602  oemapwe  9603  dfac8b  9941  fin23lem27  10238  om2uzoi  13878  ltweuz  13884  om2noseqoi  28299  wepwso  43285  onfrALTlem3  44785  onfrALTlem3VD  45127