This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniintsn

Description: Two ways to express " A is a singleton". See also en1 , en1b , card1 , and eusn . (Contributed by NM, 2-Aug-2010)

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

Proof

Step Hyp Ref Expression
1 vn0 
 |-  _V =/= (/)
2 inteq 
 |-  ( A = (/) -> |^| A = |^| (/) )
3 int0 
 |-  |^| (/) = _V
4 2 3 eqtrdi 
 |-  ( A = (/) -> |^| A = _V )
5 4 adantl 
 |-  ( ( U. A = |^| A /\ A = (/) ) -> |^| A = _V )
6 unieq 
 |-  ( A = (/) -> U. A = U. (/) )
7 uni0 
 |-  U. (/) = (/)
8 6 7 eqtrdi 
 |-  ( A = (/) -> U. A = (/) )
9 eqeq1 
 |-  ( U. A = |^| A -> ( U. A = (/) <-> |^| A = (/) ) )
10 8 9 imbitrid 
 |-  ( U. A = |^| A -> ( A = (/) -> |^| A = (/) ) )
11 10 imp 
 |-  ( ( U. A = |^| A /\ A = (/) ) -> |^| A = (/) )
12 5 11 eqtr3d 
 |-  ( ( U. A = |^| A /\ A = (/) ) -> _V = (/) )
13 12 ex 
 |-  ( U. A = |^| A -> ( A = (/) -> _V = (/) ) )
14 13 necon3d 
 |-  ( U. A = |^| A -> ( _V =/= (/) -> A =/= (/) ) )
15 1 14 mpi 
 |-  ( U. A = |^| A -> A =/= (/) )
16 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
17 15 16 sylib 
 |-  ( U. A = |^| A -> E. x x e. A )
18 vex 
 |-  x e. _V
19 vex 
 |-  y e. _V
20 18 19 prss 
 |-  ( ( x e. A /\ y e. A ) <-> { x , y } C_ A )
21 uniss 
 |-  ( { x , y } C_ A -> U. { x , y } C_ U. A )
22 21 adantl 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ U. A )
23 simpl 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. A = |^| A )
24 22 23 sseqtrd 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ |^| A )
25 intss 
 |-  ( { x , y } C_ A -> |^| A C_ |^| { x , y } )
26 25 adantl 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> |^| A C_ |^| { x , y } )
27 24 26 sstrd 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> U. { x , y } C_ |^| { x , y } )
28 18 19 unipr 
 |-  U. { x , y } = ( x u. y )
29 18 19 intpr 
 |-  |^| { x , y } = ( x i^i y )
30 27 28 29 3sstr3g 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> ( x u. y ) C_ ( x i^i y ) )
31 inss1 
 |-  ( x i^i y ) C_ x
32 ssun1 
 |-  x C_ ( x u. y )
33 31 32 sstri 
 |-  ( x i^i y ) C_ ( x u. y )
34 eqss 
 |-  ( ( 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 
 |-  ( ( x u. y ) = ( x i^i y ) <-> x = y )
36 34 35 bitr3i 
 |-  ( ( ( x u. y ) C_ ( x i^i y ) /\ ( x i^i y ) C_ ( x u. y ) ) <-> x = y )
37 30 33 36 sylanblc 
 |-  ( ( U. A = |^| A /\ { x , y } C_ A ) -> x = y )
38 37 ex 
 |-  ( U. A = |^| A -> ( { x , y } C_ A -> x = y ) )
39 20 38 biimtrid 
 |-  ( U. A = |^| A -> ( ( x e. A /\ y e. A ) -> x = y ) )
40 39 alrimivv 
 |-  ( U. A = |^| A -> A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) )
41 17 40 jca 
 |-  ( U. A = |^| A -> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
42 euabsn 
 |-  ( E! x x e. A <-> E. x { x | x e. A } = { x } )
43 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
44 43 eu4 
 |-  ( E! x x e. A <-> ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) )
45 abid2 
 |-  { x | x e. A } = A
46 45 eqeq1i 
 |-  ( { x | x e. A } = { x } <-> A = { x } )
47 46 exbii 
 |-  ( E. x { x | x e. A } = { x } <-> E. x A = { x } )
48 42 44 47 3bitr3i 
 |-  ( ( E. x x e. A /\ A. x A. y ( ( x e. A /\ y e. A ) -> x = y ) ) <-> E. x A = { x } )
49 41 48 sylib 
 |-  ( U. A = |^| A -> E. x A = { x } )
50 unisnv 
 |-  U. { x } = x
51 unieq 
 |-  ( A = { x } -> U. A = U. { x } )
52 inteq 
 |-  ( A = { x } -> |^| A = |^| { x } )
53 18 intsn 
 |-  |^| { x } = x
54 52 53 eqtrdi 
 |-  ( A = { x } -> |^| A = x )
55 50 51 54 3eqtr4a 
 |-  ( A = { x } -> U. A = |^| A )
56 55 exlimiv 
 |-  ( E. x A = { x } -> U. A = |^| A )
57 49 56 impbii 
 |-  ( U. A = |^| A <-> E. x A = { x } )