Theorem uniintsn 3253

Description: Two ways to express "A is a singleton." See also en1 5485, card1 5983, and eusn 3096.

Assertion

Ref	Expression
uniintsn	|- (U.A = |^|A <-> E.x A = {x})

Distinct variable group:   x,A

Proof of Theorem uniintsn

Step	Hyp	Ref	Expression
1		vn0 2882	. . . . . 6 |- _V =/= (/)
2		inteq 3217	. . . . . . . . . . 11 |- (A = (/) -> |^|A = |^|(/))
3		int0 3230	. . . . . . . . . . 11 |- |^|(/) = _V
4	2, 3	syl6eq 1944	. . . . . . . . . 10 |- (A = (/) -> |^|A = _V)
5	4	adantl 424	. . . . . . . . 9 |- ((U.A = |^|A /\ A = (/)) -> |^|A = _V)
6		eqeq1 1890	. . . . . . . . . . 11 |- (U.A = |^|A -> (U.A = (/) <-> |^|A = (/)))
7		unieq 3185	. . . . . . . . . . . 12 |- (A = (/) -> U.A = U.(/))
8		uni0 3205	. . . . . . . . . . . 12 |- U.(/) = (/)
9	7, 8	syl6eq 1944	. . . . . . . . . . 11 |- (A = (/) -> U.A = (/))
10	6, 9	syl5bi 225	. . . . . . . . . 10 |- (U.A = |^|A -> (A = (/) -> |^|A = (/)))
11	10	imp 377	. . . . . . . . 9 |- ((U.A = |^|A /\ A = (/)) -> |^|A = (/))
12	5, 11	eqtr3d 1927	. . . . . . . 8 |- ((U.A = |^|A /\ A = (/)) -> _V = (/))
13	12	ex 402	. . . . . . 7 |- (U.A = |^|A -> (A = (/) -> _V = (/)))
14	13	necon3d 2041	. . . . . 6 |- (U.A = |^|A -> (_V =/= (/) -> A =/= (/)))
15	1, 14	mpi 55	. . . . 5 |- (U.A = |^|A -> A =/= (/))
16		n0 2884	. . . . 5 |- (A =/= (/) <-> E.x x e. A)
17	15, 16	sylib 215	. . . 4 |- (U.A = |^|A -> E.x x e. A)
18		uniss 3199	. . . . . . . . . . . . 13 |- ({x, y} C_ A -> U.{x, y} C_ U.A)
19	18	adantl 424	. . . . . . . . . . . 12 |- ((U.A = |^|A /\ {x, y} C_ A) -> U.{x, y} C_ U.A)
20		simpl 346	. . . . . . . . . . . 12 |- ((U.A = |^|A /\ {x, y} C_ A) -> U.A = |^|A)
21	19, 20	sseqtrd 2653	. . . . . . . . . . 11 |- ((U.A = |^|A /\ {x, y} C_ A) -> U.{x, y} C_ |^|A)
22		intss 3239	. . . . . . . . . . . 12 |- ({x, y} C_ A -> |^|A C_ |^|{x, y})
23	22	adantl 424	. . . . . . . . . . 11 |- ((U.A = |^|A /\ {x, y} C_ A) -> |^|A C_ |^|{x, y})
24	21, 23	sstrd 2627	. . . . . . . . . 10 |- ((U.A = |^|A /\ {x, y} C_ A) -> U.{x, y} C_ |^|{x, y})
25		visset 2295	. . . . . . . . . . 11 |- x e. _V
26		visset 2295	. . . . . . . . . . 11 |- y e. _V
27	25, 26	unipr 3191	. . . . . . . . . 10 |- U.{x, y} = (x u. y)
28	25, 26	intpr 3250	. . . . . . . . . 10 |- |^|{x, y} = (x i^i y)
29	24, 27, 28	3sstr3g 2657	. . . . . . . . 9 |- ((U.A = |^|A /\ {x, y} C_ A) -> (x u. y) C_ (x i^i y))
30		inss1 2812	. . . . . . . . . 10 |- (x i^i y) C_ x
31		ssun1 2767	. . . . . . . . . 10 |- x C_ (x u. y)
32	30, 31	sstri 2626	. . . . . . . . 9 |- (x i^i y) C_ (x u. y)
33	29, 32	jctir 317	. . . . . . . 8 |- ((U.A = |^|A /\ {x, y} C_ A) -> ((x u. y) C_ (x i^i y) /\ (x i^i y) C_ (x u. y)))
34		eqss 2631	. . . . . . . . 9 |- ((x u. y) = (x i^i y) <-> ((x u. y) C_ (x i^i y) /\ (x i^i y) C_ (x u. y)))
35		uneqin 2845	. . . . . . . . 9 |- ((x u. y) = (x i^i y) <-> x = y)
36	34, 35	bitr3i 192	. . . . . . . 8 |- (((x u. y) C_ (x i^i y) /\ (x i^i y) C_ (x u. y)) <-> x = y)
37	33, 36	sylib 215	. . . . . . 7 |- ((U.A = |^|A /\ {x, y} C_ A) -> x = y)
38	37	ex 402	. . . . . 6 |- (U.A = |^|A -> ({x, y} C_ A -> x = y))
39	25, 26	prss 3138	. . . . . 6 |- ((x e. A /\ y e. A) <-> {x, y} C_ A)
40	38, 39	syl5ib 223	. . . . 5 |- (U.A = |^|A -> ((x e. A /\ y e. A) -> x = y))
41	40	19.21aivv 1665	. . . 4 |- (U.A = |^|A -> A.xA.y((x e. A /\ y e. A) -> x = y))
42	17, 41	jca 310	. . 3 |- (U.A = |^|A -> (E.x x e. A /\ A.xA.y((x e. A /\ y e. A) -> x = y)))
43		euabsn 3095	. . . 4 |- (E!x x e. A <-> E.x{x | x e. A} = {x})
44		eleq1 1957	. . . . 5 |- (x = y -> (x e. A <-> y e. A))
45	44	eu4 1806	. . . 4 |- (E!x x e. A <-> (E.x x e. A /\ A.xA.y((x e. A /\ y e. A) -> x = y)))
46		abid2 2011	. . . . . 6 |- {x | x e. A} = A
47	46	eqeq1i 1891	. . . . 5 |- ({x | x e. A} = {x} <-> A = {x})
48	47	exbii 1398	. . . 4 |- (E.x{x | x e. A} = {x} <-> E.x A = {x})
49	43, 45, 48	3bitr3i 198	. . 3 |- ((E.x x e. A /\ A.xA.y((x e. A /\ y e. A) -> x = y)) <-> E.x A = {x})
50	42, 49	sylib 215	. 2 |- (U.A = |^|A -> E.x A = {x})
51	25	unisn 3193	. . . 4 |- U.{x} = x
52		unieq 3185	. . . 4 |- (A = {x} -> U.A = U.{x})
53		inteq 3217	. . . . 5 |- (A = {x} -> |^|A = |^|{x})
54	25	intsn 3252	. . . . 5 |- |^|{x} = x
55	53, 54	syl6eq 1944	. . . 4 |- (A = {x} -> |^|A = x)
56	51, 52, 55	3eqtr4a 1954	. . 3 |- (A = {x} -> U.A = |^|A)
57	56	19.23aiv 1674	. 2 |- (E.x A = {x} -> U.A = |^|A)
58	50, 57	impbii 174	1 |- (U.A = |^|A <-> E.x A = {x})

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  {cab 1871   =/= wne 2017  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  {cpr 3045  U.cuni 3177  |^|cint 3214

This theorem is referenced by:  eufromeq6 3833

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-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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-sn 3049  df-pr 3050  df-uni 3178  df-int 3215

Copyright terms: Public domain