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

Theorem intex 4065
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
StepHypRef Expression
1 n0 3371 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3775 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2730 . . . . . 6  |-  x  e. 
_V
43ssex 4055 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 17 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 2023 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 189 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4049 . . . 4  |-  -.  _V  e.  _V
9 inteq 3763 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3774 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2301 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2319 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 296 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2457 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 182 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537    = wceq 1619    e. wcel 1621    =/= wne 2412   _Vcvv 2727    C_ wss 3078   (/)c0 3362   |^|cint 3760
This theorem is referenced by:  intnex  4066  intexab  4067  iinexg  4069  onint0  4478  onintrab  4483  onmindif2  4494  fival  7050  elfi2  7052  elfir  7053  dffi2  7060  elfiun  7067  fifo  7069  tz9.1c  7296  tz9.12lem1  7343  tz9.12lem3  7345  rankf  7350  cardf2  7460  cardval3  7469  cardid2  7470  cardcf  7762  cflim2  7773  intwun  8237  wuncval  8244  inttsk  8276  intgru  8316  gruina  8320  mremre  13378  mrcval  13384  asplss  15901  aspsubrg  15903  toponmre  16662  subbascn  16816  dfrtrcl2  23216  dfon2lem8  23314  dfon2lem9  23315  toplat  24456  istopx  24713  prtoptop  24715  indcls2  25162  igenval  25852  elrfi  25935  ismrcd1  25939  mzpval  25976  dmmzp  25977  pclvalN  28768
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363  df-int 3761
  Copyright terms: Public domain W3C validator