Theorem fobigcup

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

	Ref	Expression
Assertion	fobigcup	⊢ Bigcup : V –onto→ V

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝑥 ∈ V → ∪ 𝑥 ∈ V )
2	1	rgen	⊢ ∀ 𝑥 ∈ V ∪ 𝑥 ∈ V
3		dfbigcup2	⊢ Bigcup = ( 𝑥 ∈ V ↦ ∪ 𝑥 )
4	3	mptfng	⊢ ( ∀ 𝑥 ∈ V ∪ 𝑥 ∈ V ↔ Bigcup Fn V )
5	2 4	mpbi	⊢ Bigcup Fn V
6	3	rnmpt	⊢ ran Bigcup = { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 }
7		vex	⊢ 𝑦 ∈ V
8		snex	⊢ { 𝑦 } ∈ V
9	7	unisn	⊢ ∪ { 𝑦 } = 𝑦
10	9	eqcomi	⊢ 𝑦 = ∪ { 𝑦 }
11		unieq	⊢ ( 𝑥 = { 𝑦 } → ∪ 𝑥 = ∪ { 𝑦 } )
12	11	rspceeqv	⊢ ( ( { 𝑦 } ∈ V ∧ 𝑦 = ∪ { 𝑦 } ) → ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 )
13	8 10 12	mp2an	⊢ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥
14	7 13	2th	⊢ ( 𝑦 ∈ V ↔ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 )
15	14	abbi2i	⊢ V = { 𝑦 ∣ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 }
16	6 15	eqtr4i	⊢ ran Bigcup = V
17		df-fo	⊢ ( Bigcup : V –onto→ V ↔ ( Bigcup Fn V ∧ ran Bigcup = V ) )
18	5 16 17	mpbir2an	⊢ Bigcup : V –onto→ V