Theorem onelss 3705

Description: An element of an ordinal number is a subset of the number. (The proof was shortened by Andrew Salmon, 25-Jul-2011.)

Assertion

Ref	Expression
onelss	|- (A e. On -> (B e. A -> B C_ A))

Proof of Theorem onelss

Step	Hyp	Ref	Expression
1		eloni 3667	. 2 |- (A e. On -> Ord A)
2		ordelss 3674	. . 3 |- ((Ord A /\ B e. A) -> B C_ A)
3	2	ex 402	. 2 |- (Ord A -> (B e. A -> B C_ A))
4	1, 3	syl 12	1 |- (A e. On -> (B e. A -> B C_ A))

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

This theorem is referenced by:  ordunidif 3712  onelssi 3778  snsn0nonOLD 3789  ssorduni 3870  suceloni 3894  tfrlem1 5119  tfrlem5 5123  tfrlem9 5127  tfrlem11 5129  oaordex 5240  oaass 5243  odi 5258  omass 5259  oewordri 5267  domtriord 5546  ordtypelem6 5689  hartog 5693  onsdom 5694  omsubel 5883  elomsubsd 5885  omsublim 5887  infenomsub 5889  ondomon 6008  cfub 6056  cfsuc 6063  poseq 13954  axfelem8 14038  axfelem9 14039  axfelem12 14042  dmsdtriordOLD 15360  ordtypelem6OLD 15380  hartogOLD 15384  onsdomOLD 15385  omsubelOLD 15392  elomsubsdOLD 15394  omsublimOLD 15396  infenomsubOLD 15398

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