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

Theorem intmin 4146
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 2973 . . . . 5  |-  y  e. 
_V
21elintrab 4138 . . . 4  |-  ( y  e.  |^| { x  e.  B  |  A  C_  x }  <->  A. x  e.  B  ( A  C_  x  -> 
y  e.  x ) )
3 ssid 3373 . . . . 5  |-  A  C_  A
4 sseq2 3376 . . . . . . 7  |-  ( x  =  A  ->  ( A  C_  x  <->  A  C_  A
) )
5 eleq2 2502 . . . . . . 7  |-  ( x  =  A  ->  (
y  e.  x  <->  y  e.  A ) )
64, 5imbi12d 320 . . . . . 6  |-  ( x  =  A  ->  (
( A  C_  x  ->  y  e.  x )  <-> 
( A  C_  A  ->  y  e.  A ) ) )
76rspcv 3067 . . . . 5  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  ( A  C_  A  ->  y  e.  A
) ) )
83, 7mpii 43 . . . 4  |-  ( A  e.  B  ->  ( A. x  e.  B  ( A  C_  x  -> 
y  e.  x )  ->  y  e.  A
) )
92, 8syl5bi 217 . . 3  |-  ( A  e.  B  ->  (
y  e.  |^| { x  e.  B  |  A  C_  x }  ->  y  e.  A ) )
109ssrdv 3360 . 2  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  C_  A
)
11 ssintub 4144 . . 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 3371 1  |-  ( A  e.  B  ->  |^| { x  e.  B  |  A  C_  x }  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756   A.wral 2713   {crab 2717    C_ wss 3326   |^|cint 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-rab 2722  df-v 2972  df-in 3333  df-ss 3340  df-int 4127
This theorem is referenced by:  intmin2  4153  ordintdif  4766  bm2.5ii  6415  onsucmin  6430  rankonidlem  8033  rankval4  8072  mrcid  14549  lspid  17061  aspid  17399  cldcls  18644  spanid  24748  chsupid  24813  igenidl2  28862  pclidN  33537  diaocN  34767
  Copyright terms: Public domain W3C validator