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

Metamath Proof Explorer

Theorem dfbigcup2

Description: Bigcup using maps-to notation. (Contributed by Scott Fenton, 16-Apr-2012)

Ref Expression
Assertion dfbigcup2 Bigcup = ( 𝑥 ∈ V ↦ ∪ 𝑥 )

Proof

Step Hyp Ref Expression
1 relbigcup ⊢ Rel Bigcup
2 mptrel ⊢ Rel ( 𝑥 ∈ V ↦ ∪ 𝑥 )
3 eqcom ⊢ ( ∪ 𝑦 = 𝑧 ↔ 𝑧 = ∪ 𝑦 )
4 vex ⊢ 𝑧 ∈ V
5 4 brbigcup ⊢ ( 𝑦 Bigcup 𝑧 ↔ ∪ 𝑦 = 𝑧 )
6 vex ⊢ 𝑦 ∈ V
7 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ V ↔ 𝑦 ∈ V ) )
8 unieq ⊢ ( 𝑥 = 𝑦 → ∪ 𝑥 = ∪ 𝑦 )
9 8 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑡 = ∪ 𝑥 ↔ 𝑡 = ∪ 𝑦 ) )
10 7 9 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) ↔ ( 𝑦 ∈ V ∧ 𝑡 = ∪ 𝑦 ) ) )
11 6 biantrur ⊢ ( 𝑡 = ∪ 𝑦 ↔ ( 𝑦 ∈ V ∧ 𝑡 = ∪ 𝑦 ) )
12 10 11 bitr4di ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) ↔ 𝑡 = ∪ 𝑦 ) )
13 eqeq1 ⊢ ( 𝑡 = 𝑧 → ( 𝑡 = ∪ 𝑦 ↔ 𝑧 = ∪ 𝑦 ) )
14 df-mpt ⊢ ( 𝑥 ∈ V ↦ ∪ 𝑥 ) = { ⟨ 𝑥 , 𝑡 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑡 = ∪ 𝑥 ) }
15 6 4 12 13 14 brab ⊢ ( 𝑦 ( 𝑥 ∈ V ↦ ∪ 𝑥 ) 𝑧 ↔ 𝑧 = ∪ 𝑦 )
16 3 5 15 3bitr4i ⊢ ( 𝑦 Bigcup 𝑧 ↔ 𝑦 ( 𝑥 ∈ V ↦ ∪ 𝑥 ) 𝑧 )
17 1 2 16 eqbrriv ⊢ Bigcup = ( 𝑥 ∈ V ↦ ∪ 𝑥 )