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

Metamath Proof Explorer

Theorem unisngl

Description: Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020)

Ref Expression
Hypothesis dissnref.c 
|- C = { u | E. x e. X u = { x } }
Assertion unisngl 
|- X = U. C

Proof

Step Hyp Ref Expression
1 dissnref.c 
 |-  C = { u | E. x e. X u = { x } }
2 1 unieqi 
 |-  U. C = U. { u | E. x e. X u = { x } }
3 simpl 
 |-  ( ( y e. u /\ u = { x } ) -> y e. u )
4 simpr 
 |-  ( ( y e. u /\ u = { x } ) -> u = { x } )
5 3 4 eleqtrd 
 |-  ( ( y e. u /\ u = { x } ) -> y e. { x } )
6 5 exlimiv 
 |-  ( E. u ( y e. u /\ u = { x } ) -> y e. { x } )
7 eqid 
 |-  { x } = { x }
8 vsnex 
 |-  { x } e. _V
9 eleq2 
 |-  ( u = { x } -> ( y e. u <-> y e. { x } ) )
10 eqeq1 
 |-  ( u = { x } -> ( u = { x } <-> { x } = { x } ) )
11 9 10 anbi12d 
 |-  ( u = { x } -> ( ( y e. u /\ u = { x } ) <-> ( y e. { x } /\ { x } = { x } ) ) )
12 8 11 spcev 
 |-  ( ( y e. { x } /\ { x } = { x } ) -> E. u ( y e. u /\ u = { x } ) )
13 7 12 mpan2 
 |-  ( y e. { x } -> E. u ( y e. u /\ u = { x } ) )
14 6 13 impbii 
 |-  ( E. u ( y e. u /\ u = { x } ) <-> y e. { x } )
15 velsn 
 |-  ( y e. { x } <-> y = x )
16 equcom 
 |-  ( y = x <-> x = y )
17 14 15 16 3bitri 
 |-  ( E. u ( y e. u /\ u = { x } ) <-> x = y )
18 17 rexbii 
 |-  ( E. x e. X E. u ( y e. u /\ u = { x } ) <-> E. x e. X x = y )
19 r19.42v 
 |-  ( E. x e. X ( y e. u /\ u = { x } ) <-> ( y e. u /\ E. x e. X u = { x } ) )
20 19 exbii 
 |-  ( E. u E. x e. X ( y e. u /\ u = { x } ) <-> E. u ( y e. u /\ E. x e. X u = { x } ) )
21 rexcom4 
 |-  ( E. x e. X E. u ( y e. u /\ u = { x } ) <-> E. u E. x e. X ( y e. u /\ u = { x } ) )
22 eluniab 
 |-  ( y e. U. { u | E. x e. X u = { x } } <-> E. u ( y e. u /\ E. x e. X u = { x } ) )
23 20 21 22 3bitr4ri 
 |-  ( y e. U. { u | E. x e. X u = { x } } <-> E. x e. X E. u ( y e. u /\ u = { x } ) )
24 risset 
 |-  ( y e. X <-> E. x e. X x = y )
25 18 23 24 3bitr4i 
 |-  ( y e. U. { u | E. x e. X u = { x } } <-> y e. X )
26 25 eqriv 
 |-  U. { u | E. x e. X u = { x } } = X
27 2 26 eqtr2i 
 |-  X = U. C