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

Metamath Proof Explorer

Theorem iununi

Description: A relationship involving union and indexed union. Exercise 25 of Enderton p. 33. (Contributed by NM, 25-Nov-2003) (Proof shortened by Mario Carneiro, 17-Nov-2016)

Ref Expression
Assertion iununi ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅ )
2 iunconst ⊢ ( 𝐵 ≠ ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
3 1 2 sylbir ⊢ ( ¬ 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
4 iun0 ⊢ ∪ 𝑥 ∈ 𝐵 ∅ = ∅
5 id ⊢ ( 𝐴 = ∅ → 𝐴 = ∅ )
6 5 iuneq2d ⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = ∪ 𝑥 ∈ 𝐵 ∅ )
7 4 6 5 3eqtr4a ⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
8 3 7 ja ⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴 )
9 8 eqcomd ⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → 𝐴 = ∪ 𝑥 ∈ 𝐵 𝐴 )
10 9 uneq1d ⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ( 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 ) = ( ∪ 𝑥 ∈ 𝐵 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 ) )
11 uniiun ⊢ ∪ 𝐵 = ∪ 𝑥 ∈ 𝐵 𝑥
12 11 uneq2i ⊢ ( 𝐴 ∪ ∪ 𝐵 ) = ( 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 )
13 iunun ⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ( ∪ 𝑥 ∈ 𝐵 𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥 )
14 10 12 13 3eqtr4g ⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) → ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )
15 unieq ⊢ ( 𝐵 = ∅ → ∪ 𝐵 = ∪ ∅ )
16 uni0 ⊢ ∪ ∅ = ∅
17 15 16 eqtrdi ⊢ ( 𝐵 = ∅ → ∪ 𝐵 = ∅ )
18 17 uneq2d ⊢ ( 𝐵 = ∅ → ( 𝐴 ∪ ∪ 𝐵 ) = ( 𝐴 ∪ ∅ ) )
19 un0 ⊢ ( 𝐴 ∪ ∅ ) = 𝐴
20 18 19 eqtrdi ⊢ ( 𝐵 = ∅ → ( 𝐴 ∪ ∪ 𝐵 ) = 𝐴 )
21 iuneq1 ⊢ ( 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ∪ 𝑥 ∈ ∅ ( 𝐴 ∪ 𝑥 ) )
22 0iun ⊢ ∪ 𝑥 ∈ ∅ ( 𝐴 ∪ 𝑥 ) = ∅
23 21 22 eqtrdi ⊢ ( 𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) = ∅ )
24 20 23 eqeq12d ⊢ ( 𝐵 = ∅ → ( ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) ↔ 𝐴 = ∅ ) )
25 24 biimpcd ⊢ ( ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) → ( 𝐵 = ∅ → 𝐴 = ∅ ) )
26 14 25 impbii ⊢ ( ( 𝐵 = ∅ → 𝐴 = ∅ ) ↔ ( 𝐴 ∪ ∪ 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ∪ 𝑥 ) )