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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5211   E cep 5549   We wwe 5602  Ord word 6361

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 6365

This theorem is used by:  ordfr  6377  trssord  6379  tz7.5  6383  ordelord  6384  tz7.7  6388  oieu  9537  oiid  9539  hartogslem1  9540  oemapso  9687  cantnf  9698  oemapwe  9699  dfac8b  10114  fin23lem27  10410  om2uzoi  14102  ltweuz  14108  om2noseqoi  28695  wepwso  44144  onfrALTlem3  45621  onfrALTlem3VD  45963