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

Theorem intex 4170
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 3465 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3878 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2792 . . . . . 6  |-  x  e. 
_V
43ssex 4159 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 15 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1667 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 187 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4153 . . . 4  |-  -.  _V  e.  _V
9 inteq 3866 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3877 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2332 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2350 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 294 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2492 . 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 1528    = wceq 1623    e. wcel 1685    =/= wne 2447   _Vcvv 2789    C_ wss 3153   (/)c0 3456   |^|cint 3863
This theorem is referenced by:  intnex  4171  intexab  4172  iinexg  4174  onint0  4586  onintrab  4591  onmindif2  4602  fival  7162  elfi2  7164  elfir  7165  dffi2  7172  elfiun  7179  fifo  7181  tz9.1c  7408  tz9.12lem1  7455  tz9.12lem3  7457  rankf  7462  cardf2  7572  cardval3  7581  cardid2  7582  cardcf  7874  cflim2  7885  intwun  8353  wuncval  8360  inttsk  8392  intgru  8432  gruina  8436  mremre  13502  mrcval  13508  asplss  16065  aspsubrg  16067  toponmre  16826  subbascn  16980  dfrtrcl2  23452  dfon2lem8  23550  dfon2lem9  23551  toplat  24701  istopx  24958  prtoptop  24960  indcls2  25407  igenval  26097  elrfi  26180  ismrcd1  26184  mzpval  26221  dmmzp  26222  pclvalN  29358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457  df-int 3864
  Copyright terms: Public domain W3C validator