Theorem ordwe 6375

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

Syntax hints:   → wi 4  Tr wtr 5219   E cep 5562   We wwe 5615  Ord word 6361

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 210  df-an 401  df-ord 6365

This theorem is referenced by:  ordfr  6377  trssord  6379  tz7.5  6383  ordelord  6384  tz7.7  6388  oieu  9502  oiid  9504  hartogslem1  9505  oemapso  9652  cantnf  9663  oemapwe  9664  dfac8b  10016  fin23lem27  10313  om2uzoi  13993  ltweuz  13999  om2noseqoi  28477  wepwso  43753  onfrALTlem3  45236  onfrALTlem3VD  45578