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 ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 : V ⟶ onto V

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 ↔ 𝖡𝗂𝗀𝖼𝗎𝗉 Fn V
5 2 4 mpbi ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 Fn V
6 3 rnmpt ⊢ ran ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉 = y | ∃ x ∈ V y = ⋃ 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 ∈ V y = ⋃ x
13 8 10 12 mp2an ⊢ ∃ x ∈ V y = ⋃ x
14 7 13 2th ⊢ y ∈ V ↔ ∃ x ∈ V y = ⋃ x
15 14 eqabi ⊢ V = y | ∃ x ∈ V y = ⋃ x
16 6 15 eqtr4i ⊢ ran ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉 = V
17 df-fo ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 : V ⟶ onto V ↔ 𝖡𝗂𝗀𝖼𝗎𝗉 Fn V ∧ ran ⁡ 𝖡𝗂𝗀𝖼𝗎𝗉 = V
18 5 16 17 mpbir2an ⊢ 𝖡𝗂𝗀𝖼𝗎𝗉 : V ⟶ onto V