Description: Define the Bigcup function, which, per fvbigcup , carries a set to its union. (Contributed by Scott Fenton, 11-Apr-2012)
Ref | Expression | ||
---|---|---|---|
Assertion | df-bigcup | |- Bigcup = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cbigcup | |- Bigcup |
|
1 | cvv | |- _V |
|
2 | 1 1 | cxp | |- ( _V X. _V ) |
3 | cep | |- _E |
|
4 | 1 3 | ctxp | |- ( _V (x) _E ) |
5 | 3 3 | ccom | |- ( _E o. _E ) |
6 | 5 1 | ctxp | |- ( ( _E o. _E ) (x) _V ) |
7 | 4 6 | csymdif | |- ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) |
8 | 7 | crn | |- ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) |
9 | 2 8 | cdif | |- ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) |
10 | 0 9 | wceq | |- Bigcup = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( _E o. _E ) (x) _V ) ) ) |