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

Theorem intex 4573
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 3753 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4263 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 3060 . . . . . 6  |-  x  e. 
_V
43ssex 4561 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 17 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1787 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 200 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4555 . . . 4  |-  -.  _V  e.  _V
9 inteq 4251 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4262 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2512 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2524 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 309 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2665 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 192 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1455   E.wex 1674    e. wcel 1898    =/= wne 2633   _Vcvv 3057    C_ wss 3416   (/)c0 3743   |^|cint 4248
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-v 3059  df-dif 3419  df-in 3423  df-ss 3430  df-nul 3744  df-int 4249
This theorem is referenced by:  intnex  4574  intexab  4575  iinexg  4577  onint0  6650  onintrab  6655  onmindif2  6666  fival  7952  elfi2  7954  elfir  7955  dffi2  7963  elfiun  7970  fifo  7972  tz9.1c  8240  tz9.12lem1  8284  tz9.12lem3  8286  rankf  8291  cardf2  8403  cardval3  8412  cardid2  8413  cardcf  8708  cflim2  8719  intwun  9186  wuncval  9193  inttsk  9225  intgru  9265  gruina  9269  dfrtrcl2  13174  mremre  15559  mrcval  15565  asplss  18602  aspsubrg  18604  toponmre  20158  subbascn  20319  insiga  29008  sigagenval  29011  sigagensiga  29012  dmsigagen  29015  dfon2lem8  30485  dfon2lem9  30486  igenval  32339  pclvalN  33500  elrfi  35581  ismrcd1  35585  mzpval  35619  dmmzp  35620  salgenval  38220  intsal  38227
  Copyright terms: Public domain W3C validator