MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oninton Unicode version

Theorem oninton 4628
Description: The intersection of a non-empty collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by NM, 29-Jan-1997.)
Assertion
Ref Expression
oninton  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  On )

Proof of Theorem oninton
StepHypRef Expression
1 onint 4623 . . . 4  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A )
21ex 423 . . 3  |-  ( A 
C_  On  ->  ( A  =/=  (/)  ->  |^| A  e.  A ) )
3 ssel 3208 . . 3  |-  ( A 
C_  On  ->  ( |^| A  e.  A  ->  |^| A  e.  On ) )
42, 3syld 40 . 2  |-  ( A 
C_  On  ->  ( A  =/=  (/)  ->  |^| A  e.  On ) )
54imp 418 1  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  On )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701    =/= wne 2479    C_ wss 3186   (/)c0 3489   |^|cint 3899   Oncon0 4429
This theorem is referenced by:  onintrab  4629  onnmin  4631  onminex  4635  onmindif2  4640  iinon  6399  oawordeulem  6594  nnawordex  6677  tz9.12lem1  7504  rankf  7511  cardf2  7621  cff  7919  coftr  7944  sltval2  24695  nodenselem4  24723  nocvxminlem  24729  dnnumch3lem  26291  dnnumch3  26292
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251  ax-un 4549
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-br 4061  df-opab 4115  df-tr 4151  df-eprel 4342  df-po 4351  df-so 4352  df-fr 4389  df-we 4391  df-ord 4432  df-on 4433
  Copyright terms: Public domain W3C validator