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

Theorem intex 4521
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 3721 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4214 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 3037 . . . . . 6  |-  x  e. 
_V
43ssex 4509 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1730 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 195 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4503 . . . 4  |-  -.  _V  e.  _V
9 inteq 4202 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4213 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2439 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2451 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 301 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2617 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 188 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1399   E.wex 1620    e. wcel 1826    =/= wne 2577   _Vcvv 3034    C_ wss 3389   (/)c0 3711   |^|cint 4199
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-v 3036  df-dif 3392  df-in 3396  df-ss 3403  df-nul 3712  df-int 4200
This theorem is referenced by:  intnex  4522  intexab  4523  iinexg  4525  onint0  6530  onintrab  6535  onmindif2  6546  fival  7787  elfi2  7789  elfir  7790  dffi2  7798  elfiun  7805  fifo  7807  tz9.1c  8074  tz9.12lem1  8118  tz9.12lem3  8120  rankf  8125  cardf2  8237  cardval3  8246  cardid2  8247  cardcf  8545  cflim2  8556  intwun  9024  wuncval  9031  inttsk  9063  intgru  9103  gruina  9107  dfrtrcl2  12897  mremre  15011  mrcval  15017  asplss  18091  aspsubrg  18093  toponmre  19680  subbascn  19841  insiga  28286  sigagenval  28289  sigagensiga  28290  dmsigagen  28293  dfon2lem8  29387  dfon2lem9  29388  igenval  30624  elrfi  30792  ismrcd1  30796  mzpval  30830  dmmzp  30831  pclvalN  36027
  Copyright terms: Public domain W3C validator