Metamath Proof Explorer

Theorem iuncom

Description: Commutation of indexed unions. (Contributed by NM, 18-Dec-2008)

Ref Expression
Assertion iuncom ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶

Proof

Step Hyp Ref Expression
1 rexcom ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
2 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
3 2 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 ∈ 𝐶 )
4 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
5 4 rexbii ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐶 )
6 1 3 5 3bitr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
7 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 𝐶 )
8 eliun ⊢ ( 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 ↔ ∃ 𝑦 ∈ 𝐵 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐶 )
9 6 7 8 3bitr4i ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 ↔ 𝑧 ∈ ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶 )
10 9 eqriv ⊢ ∪ 𝑥 ∈ 𝐴 ∪ 𝑦 ∈ 𝐵 𝐶 = ∪ 𝑦 ∈ 𝐵 ∪ 𝑥 ∈ 𝐴 𝐶