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

Theorem onint 4775
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 4763 . . . 4  |-  Ord  On
2 tz7.5 4602 . . . 4  |-  ( ( Ord  On  /\  A  C_  On  /\  A  =/=  (/) )  ->  E. x  e.  A  ( A  i^i  x )  =  (/) )
31, 2mp3an1 1266 . . 3  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  E. x  e.  A  ( A  i^i  x )  =  (/) )
4 ssel 3342 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  On  ->  ( x  e.  A  ->  x  e.  On ) )
54imdistani 672 . . . . . . . . . . . . . . 15  |-  ( ( A  C_  On  /\  x  e.  A )  ->  ( A  C_  On  /\  x  e.  On ) )
6 ssel 3342 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
C_  On  ->  ( z  e.  A  ->  z  e.  On ) )
7 ontri1 4615 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  On  /\  z  e.  On )  ->  ( x  C_  z  <->  -.  z  e.  x ) )
8 ssel 3342 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( x 
C_  z  ->  (
y  e.  x  -> 
y  e.  z ) )
97, 8syl6bir 221 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  On  /\  z  e.  On )  ->  ( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) )
109ex 424 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  On  ->  (
z  e.  On  ->  ( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) ) )
116, 10sylan9 639 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  C_  On  /\  x  e.  On )  ->  (
z  e.  A  -> 
( -.  z  e.  x  ->  ( y  e.  x  ->  y  e.  z ) ) ) )
1211com4r 82 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  x  ->  (
( A  C_  On  /\  x  e.  On )  ->  ( z  e.  A  ->  ( -.  z  e.  x  ->  y  e.  z ) ) ) )
1312imp31 422 . . . . . . . . . . . . . . . . 17  |-  ( ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  On ) )  /\  z  e.  A )  ->  ( -.  z  e.  x  ->  y  e.  z ) )
1413ralimdva 2784 . . . . . . . . . . . . . . . 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 3668 . . . . . . . . . . . . . . . 16  |-  ( ( A  i^i  x )  =  (/)  <->  A. z  e.  A  -.  z  e.  x
)
16 vex 2959 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
1716elint2 4057 . . . . . . . . . . . . . . . 16  |-  ( y  e.  |^| A  <->  A. z  e.  A  y  e.  z )
1814, 15, 173imtr4g 262 . . . . . . . . . . . . . . 15  |-  ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  On )
)  ->  ( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A ) )
195, 18sylan2 461 . . . . . . . . . . . . . 14  |-  ( ( y  e.  x  /\  ( A  C_  On  /\  x  e.  A )
)  ->  ( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A ) )
2019exp32 589 . . . . . . . . . . . . 13  |-  ( y  e.  x  ->  ( A  C_  On  ->  (
x  e.  A  -> 
( ( A  i^i  x )  =  (/)  ->  y  e.  |^| A
) ) ) )
2120com4l 80 . . . . . . . . . . . 12  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  (
y  e.  x  -> 
y  e.  |^| A
) ) ) )
2221imp32 423 . . . . . . . . . . 11  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( y  e.  x  ->  y  e.  |^| A ) )
2322ssrdv 3354 . . . . . . . . . 10  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  C_  |^| A
)
24 intss1 4065 . . . . . . . . . . 11  |-  ( x  e.  A  ->  |^| A  C_  x )
2524ad2antrl 709 . . . . . . . . . 10  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  |^| A  C_  x
)
2623, 25eqssd 3365 . . . . . . . . 9  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  =  |^| A )
2726eleq1d 2502 . . . . . . . 8  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( x  e.  A  <->  |^| A  e.  A
) )
2827biimpd 199 . . . . . . 7  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  ( x  e.  A  ->  |^| A  e.  A ) )
2928exp32 589 . . . . . 6  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  (
x  e.  A  ->  |^| A  e.  A ) ) ) )
3029com34 79 . . . . 5  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
x  e.  A  -> 
( ( A  i^i  x )  =  (/)  ->  |^| A  e.  A
) ) ) )
3130pm2.43d 46 . . . 4  |-  ( A 
C_  On  ->  ( x  e.  A  ->  (
( A  i^i  x
)  =  (/)  ->  |^| A  e.  A ) ) )
3231rexlimdv 2829 . . 3  |-  ( A 
C_  On  ->  ( E. x  e.  A  ( A  i^i  x )  =  (/)  ->  |^| A  e.  A ) )
333, 32syl5 30 . 2  |-  ( A 
C_  On  ->  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A ) )
3433anabsi5 791 1  |-  ( ( A  C_  On  /\  A  =/=  (/) )  ->  |^| A  e.  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 359    = wceq 1652    e. wcel 1725    =/= wne 2599   A.wral 2705   E.wrex 2706    i^i cin 3319    C_ wss 3320   (/)c0 3628   |^|cint 4050   Ord word 4580   Oncon0 4581
This theorem is referenced by:  onint0  4776  onssmin  4777  onminesb  4778  onminsb  4779  oninton  4780  oneqmin  4785  oeeulem  6844  nnawordex  6880  unblem1  7359  unblem2  7360  tz9.12lem3  7715  scott0  7810  cardid2  7840  ackbij1lem18  8117  cardcf  8132  cff1  8138  cflim2  8143  cfss  8145  cofsmo  8149  fin23lem26  8205  pwfseqlem3  8535  gruina  8693  2ndcdisj  17519  sltval2  25611  nocvxmin  25646  nobndlem5  25651  rankeq1o  26112  dnnumch3  27122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-br 4213  df-opab 4267  df-tr 4303  df-eprel 4494  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585
  Copyright terms: Public domain W3C validator