Theorem intex 3465

Description: The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse.

Assertion

Ref	Expression
intex	|- (A =/= (/) <-> |^|A e. _V)

Proof of Theorem intex

Step	Hyp	Ref	Expression
1		n0 2884	. . 3 |- (A =/= (/) <-> E.x x e. A)
2		intss1 3231	. . . . 5 |- (x e. A -> |^|A C_ x)
3		visset 2295	. . . . . 6 |- x e. _V
4	3	ssex 3455	. . . . 5 |- (|^|A C_ x -> |^|A e. _V)
5	2, 4	syl 12	. . . 4 |- (x e. A -> |^|A e. _V)
6	5	19.23aiv 1674	. . 3 |- (E.x x e. A -> |^|A e. _V)
7	1, 6	sylbi 216	. 2 |- (A =/= (/) -> |^|A e. _V)
8		vprc 3449	. . . 4 |- -. _V e. _V
9		inteq 3217	. . . . . 6 |- (A = (/) -> |^|A = |^|(/))
10		int0 3230	. . . . . 6 |- |^|(/) = _V
11	9, 10	syl6eq 1944	. . . . 5 |- (A = (/) -> |^|A = _V)
12	11	eleq1d 1963	. . . 4 |- (A = (/) -> (|^|A e. _V <-> _V e. _V))
13	8, 12	mtbiri 785	. . 3 |- (A = (/) -> -. |^|A e. _V)
14	13	necon2ai 2051	. 2 |- (|^|A e. _V -> A =/= (/))
15	7, 14	impbii 174	1 |- (A =/= (/) <-> |^|A e. _V)

Syntax hints:   <-> wb 163   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  _Vcvv 2292   C_ wss 2593  (/)c0 2875  |^|cint 3214

This theorem is referenced by:  intnex 3466  intexab 3467  onint0 3877  onintrab 3882  onmindif2 3893  abfii2 5652  tz9.12lem1 5770  tz9.12lem3 5772  rankval 5779  oncardon 5866  oncardid 5867  cardon 5976  cardid 5977  cardcf 6059  subbas2 8915  fiv 10212  hsupval2 10933  hsupcl 10940  dfon2lem8 13856  dfon2lem9 13857  toplat 14638  cexint2 14862  istopx 14918  tarval2 15249  intartar 15255  elfiun 15369  inficlALT 15372  hscptsscld 15434  topmtcl 15525  neificl 15841  igenval 16209

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-v 2294  df-dif 2597  df-in 2603  df-ss 2605  df-nul 2876  df-int 3215

Copyright terms: Public domain