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

Theorem intex 4169
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
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 n0 3466 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 3879 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2793 . . . . . 6  |-  x  e. 
_V
43ssex 4160 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 15 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1668 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 187 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4154 . . . 4  |-  -.  _V  e.  _V
9 inteq 3867 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 3878 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2333 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2351 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 294 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2493 . 2  |-  ( |^| A  e.  _V  ->  A  =/=  (/) )
157, 14impbii 180 1  |-  ( A  =/=  (/)  <->  |^| A  e.  _V )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1530    = wceq 1625    e. wcel 1686    =/= wne 2448   _Vcvv 2790    C_ wss 3154   (/)c0 3457   |^|cint 3864
This theorem is referenced by:  intnex  4170  intexab  4171  iinexg  4173  onint0  4589  onintrab  4594  onmindif2  4605  fival  7168  elfi2  7170  elfir  7171  dffi2  7178  elfiun  7185  fifo  7187  tz9.1c  7414  tz9.12lem1  7461  tz9.12lem3  7463  rankf  7468  cardf2  7578  cardval3  7587  cardid2  7588  cardcf  7880  cflim2  7891  intwun  8359  wuncval  8366  inttsk  8398  intgru  8438  gruina  8442  mremre  13508  mrcval  13514  asplss  16071  aspsubrg  16073  toponmre  16832  subbascn  16986  insiga  23500  sigagenval  23503  sigagensiga  23504  dmsigagen  23507  dfrtrcl2  24047  dfon2lem8  24148  dfon2lem9  24149  toplat  25301  istopx  25558  prtoptop  25560  indcls2  26007  igenval  26697  elrfi  26780  ismrcd1  26784  mzpval  26821  dmmzp  26822  pclvalN  30152
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458  df-int 3865
  Copyright terms: Public domain W3C validator