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

Theorem intex 4109
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
StepHypRef Expression
1 n0 3406 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3818 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2743 . . . . . 6  |-  x  e. 
_V
43ssex 4098 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 17 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 2024 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 189 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4092 . . . 4  |-  -.  _V  e.  _V
9 inteq 3806 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3817 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2304 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2322 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 296 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2464 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 182 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    = wceq 1619    e. wcel 1621    =/= wne 2419   _Vcvv 2740    C_ wss 3094   (/)c0 3397   |^|cint 3803
This theorem is referenced by:  intnex  4110  intexab  4111  iinexg  4113  onint0  4524  onintrab  4529  onmindif2  4540  fival  7099  elfi2  7101  elfir  7102  dffi2  7109  elfiun  7116  fifo  7118  tz9.1c  7345  tz9.12lem1  7392  tz9.12lem3  7394  rankf  7399  cardf2  7509  cardval3  7518  cardid2  7519  cardcf  7811  cflim2  7822  intwun  8290  wuncval  8297  inttsk  8329  intgru  8369  gruina  8373  mremre  13433  mrcval  13439  asplss  15996  aspsubrg  15998  toponmre  16757  subbascn  16911  dfrtrcl2  23382  dfon2lem8  23480  dfon2lem9  23481  toplat  24622  istopx  24879  prtoptop  24881  indcls2  25328  igenval  26018  elrfi  26101  ismrcd1  26105  mzpval  26142  dmmzp  26143  pclvalN  29209
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398  df-int 3804
  Copyright terms: Public domain W3C validator