Metamath Proof Explorer


Theorem fobigcup

Description: Bigcup maps the universe onto itself. (Contributed by Scott Fenton, 16-Apr-2012)

Ref Expression
Assertion fobigcup βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰:V⟢ontoV

Proof

Step Hyp Ref Expression
1 uniexg ⊒x∈V→⋃x∈V
2 1 rgen βŠ’βˆ€x∈V⋃x∈V
3 dfbigcup2 βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰=x∈VβŸΌβ‹ƒx
4 3 mptfng βŠ’βˆ€x∈V⋃x∈Vβ†”π–‘π—‚π—€π–Όπ—Žπ—‰FnV
5 2 4 mpbi βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰FnV
6 3 rnmpt ⊒ranβ‘π–‘π—‚π—€π–Όπ—Žπ—‰=y|βˆƒx∈Vy=⋃x
7 vex ⊒y∈V
8 vsnex ⊒y∈V
9 unisnv βŠ’β‹ƒy=y
10 9 eqcomi ⊒y=⋃y
11 unieq ⊒x=y→⋃x=⋃y
12 11 rspceeqv ⊒y∈V∧y=⋃yβ†’βˆƒx∈Vy=⋃x
13 8 10 12 mp2an βŠ’βˆƒx∈Vy=⋃x
14 7 13 2th ⊒y∈Vβ†”βˆƒx∈Vy=⋃x
15 14 eqabi ⊒V=y|βˆƒx∈Vy=⋃x
16 6 15 eqtr4i ⊒ranβ‘π–‘π—‚π—€π–Όπ—Žπ—‰=V
17 df-fo βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰:V⟢ontoVβ†”π–‘π—‚π—€π–Όπ—Žπ—‰FnV∧ranβ‘π–‘π—‚π—€π–Όπ—Žπ—‰=V
18 5 16 17 mpbir2an βŠ’π–‘π—‚π—€π–Όπ—Žπ—‰:V⟢ontoV