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

Theorem intmin 4268
Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
intmin  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  =  A )
Distinct variable groups:    x, A    x, B

Proof of Theorem intmin
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 vex 3060 . . . . 5  |-  y  e. 
_V
21elintrab 4260 . . . 4  |-  ( y  e.  |^| { x  e.  B  |  A  C_  x }  <->  A. x  e.  B  ( A  C_  x  -> 
y  e.  x ) )
3 ssid 3463 . . . . 5  |-  A  C_  A
4 sseq2 3466 . . . . . . 7  |-  ( x  =  A  ->  ( A  C_  x  <->  A  C_  A
) )
5 eleq2 2529 . . . . . . 7  |-  ( x  =  A  ->  (
y  e.  x  <->  y  e.  A ) )
64, 5imbi12d 326 . . . . . 6  |-  ( x  =  A  ->  (
( A  C_  x  ->  y  e.  x )  <-> 
( A  C_  A  ->  y  e.  A ) ) )
76rspcv 3158 . . . . 5  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  ( A  C_  A  ->  y  e.  A
) ) )
83, 7mpii 44 . . . 4  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  y  e.  A
) )
92, 8syl5bi 225 . . 3  |-  ( A  e.  B  ->  (
y  e.  |^| { x  e.  B  |  A  C_  x }  ->  y  e.  A ) )
109ssrdv 3450 . 2  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  C_  A
)
11 ssintub 4266 . . 3  |-  A  C_  |^|
{ x  e.  B  |  A  C_  x }
1211a1i 11 . 2  |-  ( A  e.  B  ->  A  C_ 
|^| { x  e.  B  |  A  C_  x }
)
1310, 12eqssd 3461 1  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1455    e. wcel 1898   A.wral 2749   {crab 2753    C_ wss 3416   |^|cint 4248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rab 2758  df-v 3059  df-in 3423  df-ss 3430  df-int 4249
This theorem is referenced by:  intmin2  4276  ordintdif  5495  bm2.5ii  6665  onsucmin  6680  rankonidlem  8330  rankval4  8369  mrcid  15574  lspid  18260  aspid  18609  cldcls  20112  spanid  27056  chsupid  27121  igenidl2  32344  pclidN  33507  diaocN  34739
  Copyright terms: Public domain W3C validator