Theorem eloni 3667

Description: An ordinal number has the ordinal property.

Assertion

Ref	Expression
eloni	|- (A e. On -> Ord A)

Proof of Theorem eloni

Step	Hyp	Ref	Expression
1		elong 3665	. 2 |- (A e. On -> (A e. On <-> Ord A))
2	1	ibi 652	1 |- (A e. On -> Ord A)

Syntax hints:   -> wi 3   e. wcel 1300  Ord word 3656  Oncon0 3657

This theorem is referenced by:  elon2 3668  onelon 3683  onin 3690  ontri1 3695  onelpss 3703  onsseleq 3704  onelss 3705  onelssOLD 3706  ontr1 3710  ontr2 3711  ordunidif 3712  on0eln0 3718  ordsssuc 3756  onsssuc 3757  onnbtwn 3762  suc11 3773  onordi 3774  onssneli 3779  ordon 3863  ordeleqon 3866  onss 3869  ssorduniOLD 3871  ordsuc 3895  onpwsuc 3897  onsucmin 3901  ordunisuc 3911  ordunisucOLD 3912  onsucuni2 3914  onsucuni2OLD 3915  onuninsuci 3921  ordunisuc2 3926  ordzsl 3927  onzsl 3928  nlimon 3935  tfinds 3942  tfindsOLD 3943  tfindsg2 3945  nnord 3959  onfununi 5116  tz7.48lem 5164  oe0m1 5205  oesuc 5211  oaordi 5227  oaord 5228  oacan 5229  oawordri 5232  oalimcl 5242  oaass 5243  omord2 5246  omcan 5248  omwordi 5250  omword1 5252  omword2 5253  om00 5254  omlimcl 5257  omass 5259  oen0 5261  oeord 5263  oecan 5264  oewordi 5266  oeworde 5268  nnarcl 5287  oaabs 5309  omsmo 5314  domtriord 5546  onomeneq 5612  ordtypelem7 5690  hartog 5693  onsdom 5694  infensuc 5745  r1ord 5766  r1val1 5769  rankr1 5785  rankval3 5792  bndrank 5793  r1pw 5797  rankbnd2 5815  cardnn 5870  omsubsuc2 5878  omsubsdom 5881  omsubdom 5882  omsubel 5883  omsubss 5884  elomsubsd 5885  omsubdmss 5886  omsublim 5887  infenomsub 5889  weth 5949  zorn2lem6 5955  ondomcard 6009  carduni 6010  cardaleph 6033  iscard3 6036  alephfp 6048  ordsucuniel 13863  poseq 13954  soseq 13955  nodmord 13996  axdenselem2 14020  axdenselem4 14022  axdenselem5 14023  axfelem11 14041  axfelem15 14045  axfelem16 14046  ordsuccl2 14431  ordsuccl3 14432  celsor 14443  vtarl 15264  tartarmap 15265  eltintpar 15276  inttaror 15277  dmsdtriordOLD 15360  ordtypelem7OLD 15381  hartogOLD 15384  onsdomOLD 15385  omsubsuc2OLD 15387  omsubsdomOLD 15390  omsubdomOLD 15391  omsubelOLD 15392  omsubssOLD 15393  elomsubsdOLD 15394  omsubdmssOLD 15395  omsublimOLD 15396  infenomsubOLD 15398  smoge 16454

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178  df-tr 3412  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661

Copyright terms: Public domain