Metamath Proof Explorer
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 × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) ) |
Detailed syntax breakdown
| Step |
Hyp |
Ref |
Expression |
| 0 |
|
cbigcup |
⊢ Bigcup |
| 1 |
|
cvv |
⊢ V |
| 2 |
1 1
|
cxp |
⊢ ( V × V ) |
| 3 |
|
cep |
⊢ E |
| 4 |
1 3
|
ctxp |
⊢ ( V ⊗ E ) |
| 5 |
3 3
|
ccom |
⊢ ( E ∘ E ) |
| 6 |
5 1
|
ctxp |
⊢ ( ( E ∘ E ) ⊗ V ) |
| 7 |
4 6
|
csymdif |
⊢ ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) |
| 8 |
7
|
crn |
⊢ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) |
| 9 |
2 8
|
cdif |
⊢ ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) ) |
| 10 |
0 9
|
wceq |
⊢ Bigcup = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( ( E ∘ E ) ⊗ V ) ) ) |