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

Theorem intex 4448
Description: The intersection of a nonempty 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 3646 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4143 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2975 . . . . . 6  |-  x  e. 
_V
43ssex 4436 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1688 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 195 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4430 . . . 4  |-  -.  _V  e.  _V
9 inteq 4131 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4142 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2491 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2509 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 303 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2656 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 188 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2606   _Vcvv 2972    C_ wss 3328   (/)c0 3637   |^|cint 4128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-v 2974  df-dif 3331  df-in 3335  df-ss 3342  df-nul 3638  df-int 4129
This theorem is referenced by:  intnex  4449  intexab  4450  iinexg  4452  onint0  6407  onintrab  6412  onmindif2  6423  fival  7662  elfi2  7664  elfir  7665  dffi2  7673  elfiun  7680  fifo  7682  tz9.1c  7950  tz9.12lem1  7994  tz9.12lem3  7996  rankf  8001  cardf2  8113  cardval3  8122  cardid2  8123  cardcf  8421  cflim2  8432  intwun  8902  wuncval  8909  inttsk  8941  intgru  8981  gruina  8985  mremre  14542  mrcval  14548  asplss  17400  aspsubrg  17402  toponmre  18697  subbascn  18858  insiga  26580  sigagenval  26583  sigagensiga  26584  dmsigagen  26587  dfrtrcl2  27350  dfon2lem8  27603  dfon2lem9  27604  igenval  28861  elrfi  29030  ismrcd1  29034  mzpval  29068  dmmzp  29069  pclvalN  33534
  Copyright terms: Public domain W3C validator