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

Theorem intex 4348
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 3629 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4057 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2951 . . . . . 6  |-  x  e. 
_V
43ssex 4339 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1644 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 188 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4333 . . . 4  |-  -.  _V  e.  _V
9 inteq 4045 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4056 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2483 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2501 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 295 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2643 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 181 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550    = wceq 1652    e. wcel 1725    =/= wne 2598   _Vcvv 2948    C_ wss 3312   (/)c0 3620   |^|cint 4042
This theorem is referenced by:  intnex  4349  intexab  4350  iinexg  4352  onint0  4768  onintrab  4773  onmindif2  4784  fival  7409  elfi2  7411  elfir  7412  dffi2  7420  elfiun  7427  fifo  7429  tz9.1c  7658  tz9.12lem1  7705  tz9.12lem3  7707  rankf  7712  cardf2  7822  cardval3  7831  cardid2  7832  cardcf  8124  cflim2  8135  intwun  8602  wuncval  8609  inttsk  8641  intgru  8681  gruina  8685  mremre  13821  mrcval  13827  asplss  16380  aspsubrg  16382  toponmre  17149  subbascn  17310  insiga  24512  sigagenval  24515  sigagensiga  24516  dmsigagen  24519  dfrtrcl2  25140  dfon2lem8  25409  dfon2lem9  25410  igenval  26652  elrfi  26729  ismrcd1  26733  mzpval  26770  dmmzp  26771  pclvalN  30614
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326  df-nul 3621  df-int 4043
  Copyright terms: Public domain W3C validator