Theorem ordwe 6401

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

This proof depends on syntax axioms:   → wi 4  Tr wtr 5218   E cep 5557   We wwe 5610  Ord word 6387

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 6391

This theorem is used by:  ordfr  6403  trssord  6405  tz7.5  6409  ordelord  6410  tz7.7  6414  oieu  9570  oiid  9572  hartogslem1  9573  oemapso  9720  cantnf  9731  oemapwe  9732  dfac8b  10149  fin23lem27  10445  om2uzoi  14138  ltweuz  14144  om2noseqoi  28746  wepwso  44316  onfrALTlem3  45787  onfrALTlem3VD  46129  hfstructwe  46303