Theorem ordwe 6199

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

Syntax hints:   → wi 4  Tr wtr 5165   E cep 5459   We wwe 5508  Ord word 6185

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 209  df-an 399  df-ord 6189

This theorem is referenced by:  ordfr  6201  trssord  6203  tz7.5  6207  ordelord  6208  tz7.7  6212  oieu  8997  oiid  8999  hartogslem1  9000  oemapso  9139  cantnf  9150  oemapwe  9151  dfac8b  9451  fin23lem27  9744  om2uzoi  13317  ltweuz  13323  wepwso  39636  onfrALTlem3  40871  onfrALTlem3VD  41214