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

Theorem intex 4603
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 3794 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4297 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 3116 . . . . . 6  |-  x  e. 
_V
43ssex 4591 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1698 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 195 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4585 . . . 4  |-  -.  _V  e.  _V
9 inteq 4285 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4296 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2524 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2536 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 303 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2702 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 188 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379   E.wex 1596    e. wcel 1767    =/= wne 2662   _Vcvv 3113    C_ wss 3476   (/)c0 3785   |^|cint 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-v 3115  df-dif 3479  df-in 3483  df-ss 3490  df-nul 3786  df-int 4283
This theorem is referenced by:  intnex  4604  intexab  4605  iinexg  4607  onint0  6610  onintrab  6615  onmindif2  6626  fival  7871  elfi2  7873  elfir  7874  dffi2  7882  elfiun  7889  fifo  7891  tz9.1c  8160  tz9.12lem1  8204  tz9.12lem3  8206  rankf  8211  cardf2  8323  cardval3  8332  cardid2  8333  cardcf  8631  cflim2  8642  intwun  9112  wuncval  9119  inttsk  9151  intgru  9191  gruina  9195  mremre  14858  mrcval  14864  asplss  17765  aspsubrg  17767  toponmre  19376  subbascn  19537  insiga  27793  sigagenval  27796  sigagensiga  27797  dmsigagen  27800  dfrtrcl2  28562  dfon2lem8  28815  dfon2lem9  28816  igenval  30077  elrfi  30246  ismrcd1  30250  mzpval  30284  dmmzp  30285  pclvalN  34695
  Copyright terms: Public domain W3C validator