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

Metamath Proof Explorer

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 vsnex ⊢ { 𝑦 } ∈ V
9 unisnv ⊢ ∪ { 𝑦 } = 𝑦
10 9 eqcomi ⊢ 𝑦 = ∪ { 𝑦 }
11 unieq ⊢ ( 𝑥 = { 𝑦 } → ∪ 𝑥 = ∪ { 𝑦 } )
12 11 rspceeqv ⊢ ( ( { 𝑦 } ∈ V ∧ 𝑦 = ∪ { 𝑦 } ) → ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 )
13 8 10 12 mp2an ⊢ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥
14 7 13 2th ⊢ ( 𝑦 ∈ V ↔ ∃ 𝑥 ∈ V 𝑦 = ∪ 𝑥 )
15 14 eqabi ⊢ 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