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

Theorem intex 4143
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 3439 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3851 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2766 . . . . . 6  |-  x  e. 
_V
43ssex 4132 . . . . 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 4126 . . . 4  |-  -.  _V  e.  _V
9 inteq 3839 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3850 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2306 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2324 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 296 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2466 . 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 2421   _Vcvv 2763    C_ wss 3127   (/)c0 3430   |^|cint 3836
This theorem is referenced by:  intnex  4144  intexab  4145  iinexg  4147  onint0  4559  onintrab  4564  onmindif2  4575  fival  7134  elfi2  7136  elfir  7137  dffi2  7144  elfiun  7151  fifo  7153  tz9.1c  7380  tz9.12lem1  7427  tz9.12lem3  7429  rankf  7434  cardf2  7544  cardval3  7553  cardid2  7554  cardcf  7846  cflim2  7857  intwun  8325  wuncval  8332  inttsk  8364  intgru  8404  gruina  8408  mremre  13469  mrcval  13475  asplss  16032  aspsubrg  16034  toponmre  16793  subbascn  16947  dfrtrcl2  23418  dfon2lem8  23516  dfon2lem9  23517  toplat  24658  istopx  24915  prtoptop  24917  indcls2  25364  igenval  26054  elrfi  26137  ismrcd1  26141  mzpval  26178  dmmzp  26179  pclvalN  29329
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 2239  ax-sep 4115
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431  df-int 3837
  Copyright terms: Public domain W3C validator