Theorem ordwe 6377

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5220   E cep 5562   We wwe 5615  Ord word 6363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-ord 6367

This theorem is used by:  ordfr  6379  trssord  6381  tz7.5  6385  ordelord  6386  tz7.7  6390  oieu  9504  oiid  9506  hartogslem1  9507  oemapso  9654  cantnf  9665  oemapwe  9666  dfac8b  10027  fin23lem27  10323  om2uzoi  14004  ltweuz  14010  om2noseqoi  28525  wepwso  43803  onfrALTlem3  45286  onfrALTlem3VD  45628