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

Theorem intex 4183
Description: The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.)
Assertion
Ref Expression
intex  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )

Proof of Theorem intex
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 n0 3477 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3893 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2804 . . . . . 6  |-  x  e. 
_V
43ssex 4174 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 15 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1624 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 187 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4168 . . . 4  |-  -.  _V  e.  _V
9 inteq 3881 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3892 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2344 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2362 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 294 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2504 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 180 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531    = wceq 1632    e. wcel 1696    =/= wne 2459   _Vcvv 2801    C_ wss 3165   (/)c0 3468   |^|cint 3878
This theorem is referenced by:  intnex  4184  intexab  4185  iinexg  4187  onint0  4603  onintrab  4608  onmindif2  4619  fival  7182  elfi2  7184  elfir  7185  dffi2  7192  elfiun  7199  fifo  7201  tz9.1c  7428  tz9.12lem1  7475  tz9.12lem3  7477  rankf  7482  cardf2  7592  cardval3  7601  cardid2  7602  cardcf  7894  cflim2  7905  intwun  8373  wuncval  8380  inttsk  8412  intgru  8452  gruina  8456  mremre  13522  mrcval  13528  asplss  16085  aspsubrg  16087  toponmre  16846  subbascn  17000  insiga  23513  sigagenval  23516  sigagensiga  23517  dmsigagen  23520  dfrtrcl2  24060  dfon2lem8  24217  dfon2lem9  24218  toplat  25393  istopx  25650  prtoptop  25652  indcls2  26099  igenval  26789  elrfi  26872  ismrcd1  26876  mzpval  26913  dmmzp  26914  pclvalN  30701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469  df-int 3879
  Copyright terms: Public domain W3C validator