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

Theorem onint 4588
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 4576 . . . 4  |-  Ord  On
2 tz7.5 4415 . . . 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 3176 . . . . . . . . . . . . . . . 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 3176 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
C_  On  ->  ( z  e.  A  ->  z  e.  On ) )
7 ontri1 4428 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( x  e.  On  /\  z  e.  On )  ->  ( x  C_  z  <->  -.  z  e.  x ) )
8 ssel 3176 . . . . . . . . . . . . . . . . . . . . . 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 2623 . . . . . . . . . . . . . . . 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 3497 . . . . . . . . . . . . . . . 16  |-  ( ( A  i^i  x )  =  (/)  <->  A. z  e.  A  -.  z  e.  x
)
16 vex 2793 . . . . . . . . . . . . . . . . 17  |-  y  e. 
_V
1716elint2 3871 . . . . . . . . . . . . . . . 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 3187 . . . . . . . . . 10  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  C_  |^| A
)
24 intss1 3879 . . . . . . . . . . 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 3198 . . . . . . . . 9  |-  ( ( A  C_  On  /\  (
x  e.  A  /\  ( A  i^i  x
)  =  (/) ) )  ->  x  =  |^| A )
2726eleq1d 2351 . . . . . . . 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 2668 . . 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 1625    e. wcel 1686    =/= wne 2448   A.wral 2545   E.wrex 2546    i^i cin 3153    C_ wss 3154   (/)c0 3457   |^|cint 3864   Ord word 4393   Oncon0 4394
This theorem is referenced by:  onint0  4589  onssmin  4590  onminesb  4591  onminsb  4592  oninton  4593  oneqmin  4598  oeeulem  6601  nnawordex  6637  unblem1  7111  unblem2  7112  tz9.12lem3  7463  scott0  7558  cardid2  7588  ackbij1lem18  7865  cardcf  7880  cff1  7886  cflim2  7891  cfss  7893  cofsmo  7897  fin23lem26  7953  pwfseqlem3  8284  gruina  8442  2ndcdisj  17184  sltval2  24312  nocvxmin  24347  nobndlem5  24352  rankeq1o  24803  dnnumch3  27155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
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 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-br 4026  df-opab 4080  df-tr 4116  df-eprel 4307  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398
  Copyright terms: Public domain W3C validator