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

Theorem onint 4585
Description: The intersection (infimum) of a non-empty class of ordinal numbers belongs to the class. Compare Exercise 4 of [TakeutiZaring] p. 45. (Contributed by NM, 31-Jan-1997.)
Assertion
Ref Expression
onint  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A )

Proof of Theorem onint
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordon 4573 . . . 4  |-  Ord  On
2 tz7.5 4412 . . . 4  |-  ( ( Ord  On  /\  A  C_  On  /\  A  =/=  (/) )  ->  E. x  e.  A  ( A  i^i  x )  =  (/) )
31, 2mp3an1 1264 . . 3  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  E. x  e.  A  ( A  i^i  x )  =  (/) )
4 ssel 3175 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  On  ->  ( x  e.  A  ->  x  e.  On ) )
54imdistani 671 . . . . . . . . . . . . . . 15  |-  ( ( A  C_  On  /\  x  e.  A )  ->  ( A  C_  On  /\  x  e.  On ) )
6 ssel 3175 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
C_  On  ->  ( z  e.  A  ->  z  e.  On ) )
7 ontri1 4425 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  On  /\  z  e.  On )  ->  ( x  C_  z  <->  -.  z  e.  x ) )
8 ssel 3175 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x 
C_  z  ->  (
y  e.  x  -> 
y  e.  z ) )
97, 8syl6bir 220 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  On  /\  z  e.  On )  ->  ( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) )
109ex 423 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  On  ->  (
z  e.  On  ->  ( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) ) )
116, 10sylan9 638 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  C_  On  /\  x  e.  On )  ->  (
z  e.  A  -> 
( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) ) )
1211com4r 80 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  x  ->  (
( A  C_  On  /\  x  e.  On )  ->  ( z  e.  A  ->  ( -.  z  e.  x  ->  y  e.  z ) ) ) )
1312imp31 421 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  On ) )  /\  z  e.  A )  ->  ( -.  z  e.  x  ->  y  e.  z ) )
1413ralimdva 2622 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  On )
)  ->  ( A. z  e.  A  -.  z  e.  x  ->  A. z  e.  A  y  e.  z ) )
15 disj 3496 . . . . . . . . . . . . . . . 16  |-  ( ( A  i^i  x )  =  (/)  <->  A. z  e.  A  -.  z  e.  x
)
16 vex 2792 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
1716elint2 3870 . . . . . . . . . . . . . . . 16  |-  ( y  e.  |^| A  <->  A. z  e.  A  y  e.  z )
1814, 15, 173imtr4g 261 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  On )
)  ->  ( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A ) )
195, 18sylan2 460 . . . . . . . . . . . . . 14  |-  ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  A )
)  ->  ( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A ) )
2019exp32 588 . . . . . . . . . . . . 13  |-  ( y  e.  x  ->  ( A  C_  On  ->  (
x  e.  A  -> 
( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A
) ) ) )
2120com4l 78 . . . . . . . . . . . 12  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  (
y  e.  x  -> 
y  e.  |^| A
) ) ) )
2221imp32 422 . . . . . . . . . . 11  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( y  e.  x  ->  y  e.  |^| A ) )
2322ssrdv 3186 . . . . . . . . . 10  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  C_  |^| A
)
24 intss1 3878 . . . . . . . . . . 11  |-  ( x  e.  A  ->  |^| A  C_  x )
2524ad2antrl 708 . . . . . . . . . 10  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  |^| A  C_  x
)
2623, 25eqssd 3197 . . . . . . . . 9  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  =  |^| A )
2726eleq1d 2350 . . . . . . . 8  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( x  e.  A  <->  |^| A  e.  A
) )
2827biimpd 198 . . . . . . 7  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( x  e.  A  ->  |^| A  e.  A ) )
2928exp32 588 . . . . . 6  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  (
x  e.  A  ->  |^| A  e.  A ) ) ) )
3029com34 77 . . . . 5  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
x  e.  A  -> 
( ( A  i^i  x )  =  (/)  ->  |^| A  e.  A
) ) ) )
3130pm2.43d 44 . . . 4  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  |^| A  e.  A ) ) )
3231rexlimdv 2667 . . 3  |-  ( A 
C_  On  ->  ( E. x  e.  A  ( A  i^i  x )  =  (/)  ->  |^| A  e.  A ) )
333, 32syl5 28 . 2  |-  ( A 
C_  On  ->  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A ) )
3433anabsi5 790 1  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    = wceq 1623    e. wcel 1685    =/= wne 2447   A.wral 2544   E.wrex 2545    i^i cin 3152    C_ wss 3153   (/)c0 3456   |^|cint 3863   Ord word 4390   Oncon0 4391
This theorem is referenced by:  onint0  4586  onssmin  4587  onminesb  4588  onminsb  4589  oninton  4590  oneqmin  4595  oeeulem  6595  nnawordex  6631  unblem1  7105  unblem2  7106  tz9.12lem3  7457  scott0  7552  cardid2  7582  ackbij1lem18  7859  cardcf  7874  cff1  7880  cflim2  7885  cfss  7887  cofsmo  7891  fin23lem26  7947  pwfseqlem3  8278  gruina  8436  2ndcdisj  17178  sltval2  23713  nocvxmin  23749  axfelem5  23754  rankeq1o  24211  dnnumch3  26555
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
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 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pss 3169  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-int 3864  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-on 4395
  Copyright terms: Public domain W3C validator