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

Theorem intex 4391
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 3625 . . 3  |-  ( A  =/=  (/)  <->  E. x  x  e.  A )
2 intss1 4094 . . . . 5  |-  ( x  e.  A  ->  |^| A  C_  x )
3 vex 2968 . . . . . 6  |-  x  e. 
_V
43ssex 4382 . . . . 5  |-  ( |^| A  C_  x  ->  |^| A  e.  _V )
52, 4syl 16 . . . 4  |-  ( x  e.  A  ->  |^| A  e.  _V )
65exlimiv 1646 . . 3  |-  ( E. x  x  e.  A  ->  |^| A  e.  _V )
71, 6sylbi 189 . 2  |-  ( A  =/=  (/)  ->  |^| A  e. 
_V )
8 vprc 4376 . . . 4  |-  -.  _V  e.  _V
9 inteq 4082 . . . . . 6  |-  ( A  =  (/)  ->  |^| A  =  |^| (/) )
10 int0 4093 . . . . . 6  |-  |^| (/)  =  _V
119, 10syl6eq 2491 . . . . 5  |-  ( A  =  (/)  ->  |^| A  =  _V )
1211eleq1d 2509 . . . 4  |-  ( A  =  (/)  ->  ( |^| A  e.  _V  <->  _V  e.  _V ) )
138, 12mtbiri 296 . . 3  |-  ( A  =  (/)  ->  -.  |^| A  e.  _V )
1413necon2ai 2656 . 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 1551    = wceq 1654    e. wcel 1728    =/= wne 2606   _Vcvv 2965    C_ wss 3309   (/)c0 3616   |^|cint 4079
This theorem is referenced by:  intnex  4392  intexab  4393  iinexg  4395  onint0  4811  onintrab  4816  onmindif2  4827  fival  7453  elfi2  7455  elfir  7456  dffi2  7464  elfiun  7471  fifo  7473  tz9.1c  7702  tz9.12lem1  7749  tz9.12lem3  7751  rankf  7756  cardf2  7868  cardval3  7877  cardid2  7878  cardcf  8170  cflim2  8181  intwun  8648  wuncval  8655  inttsk  8687  intgru  8727  gruina  8731  mremre  13867  mrcval  13873  asplss  16426  aspsubrg  16428  toponmre  17195  subbascn  17356  insiga  24555  sigagenval  24558  sigagensiga  24559  dmsigagen  24562  dfrtrcl2  25183  dfon2lem8  25452  dfon2lem9  25453  igenval  26713  elrfi  26860  ismrcd1  26864  mzpval  26901  dmmzp  26902  pclvalN  30861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-v 2967  df-dif 3312  df-in 3316  df-ss 3323  df-nul 3617  df-int 4080
  Copyright terms: Public domain W3C validator