Proof of Theorem iununi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ne 2940 | . . . . . . 7
⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅) | 
| 2 |  | iunconst 5000 | . . . . . . 7
⊢ (𝐵 ≠ ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) | 
| 3 | 1, 2 | sylbir 235 | . . . . . 6
⊢ (¬
𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) | 
| 4 |  | iun0 5061 | . . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 ∅ = ∅ | 
| 5 |  | id 22 | . . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) | 
| 6 | 5 | iuneq2d 5021 | . . . . . . 7
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = ∪ 𝑥 ∈ 𝐵 ∅) | 
| 7 | 4, 6, 5 | 3eqtr4a 2802 | . . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) | 
| 8 | 3, 7 | ja 186 | . . . . 5
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) | 
| 9 | 8 | eqcomd 2742 | . . . 4
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → 𝐴 = ∪ 𝑥 ∈ 𝐵 𝐴) | 
| 10 | 9 | uneq1d 4166 | . . 3
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥)) | 
| 11 |  | uniiun 5057 | . . . 4
⊢ ∪ 𝐵 =
∪ 𝑥 ∈ 𝐵 𝑥 | 
| 12 | 11 | uneq2i 4164 | . . 3
⊢ (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) | 
| 13 |  | iunun 5092 | . . 3
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥) | 
| 14 | 10, 12, 13 | 3eqtr4g 2801 | . 2
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) | 
| 15 |  | unieq 4917 | . . . . . . 7
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∪ ∅) | 
| 16 |  | uni0 4934 | . . . . . . 7
⊢ ∪ ∅ = ∅ | 
| 17 | 15, 16 | eqtrdi 2792 | . . . . . 6
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∅) | 
| 18 | 17 | uneq2d 4167 | . . . . 5
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪
∅)) | 
| 19 |  | un0 4393 | . . . . 5
⊢ (𝐴 ∪ ∅) = 𝐴 | 
| 20 | 18, 19 | eqtrdi 2792 | . . . 4
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
𝐴) | 
| 21 |  | iuneq1 5007 | . . . . 5
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥)) | 
| 22 |  | 0iun 5062 | . . . . 5
⊢ ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥) = ∅ | 
| 23 | 21, 22 | eqtrdi 2792 | . . . 4
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∅) | 
| 24 | 20, 23 | eqeq12d 2752 | . . 3
⊢ (𝐵 = ∅ → ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) ↔ 𝐴 = ∅)) | 
| 25 | 24 | biimpcd 249 | . 2
⊢ ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) → (𝐵 = ∅ → 𝐴 = ∅)) | 
| 26 | 14, 25 | impbii 209 | 1
⊢ ((𝐵 = ∅ → 𝐴 = ∅) ↔ (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) |