Proof of Theorem iununi
Step | Hyp | Ref
| Expression |
1 | | df-ne 2936 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅) |
2 | | iunconst 4900 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
3 | 1, 2 | sylbir 238 |
. . . . . 6
⊢ (¬
𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
4 | | iun0 4957 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 ∅ = ∅ |
5 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
6 | 5 | iuneq2d 4920 |
. . . . . . 7
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = ∪ 𝑥 ∈ 𝐵 ∅) |
7 | 4, 6, 5 | 3eqtr4a 2800 |
. . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
8 | 3, 7 | ja 189 |
. . . . 5
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
9 | 8 | eqcomd 2745 |
. . . 4
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → 𝐴 = ∪ 𝑥 ∈ 𝐵 𝐴) |
10 | 9 | uneq1d 4062 |
. . 3
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥)) |
11 | | uniiun 4954 |
. . . 4
⊢ ∪ 𝐵 =
∪ 𝑥 ∈ 𝐵 𝑥 |
12 | 11 | uneq2i 4060 |
. . 3
⊢ (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) |
13 | | iunun 4988 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥) |
14 | 10, 12, 13 | 3eqtr4g 2799 |
. 2
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) |
15 | | unieq 4817 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∪ ∅) |
16 | | uni0 4836 |
. . . . . . 7
⊢ ∪ ∅ = ∅ |
17 | 15, 16 | eqtrdi 2790 |
. . . . . 6
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∅) |
18 | 17 | uneq2d 4063 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪
∅)) |
19 | | un0 4289 |
. . . . 5
⊢ (𝐴 ∪ ∅) = 𝐴 |
20 | 18, 19 | eqtrdi 2790 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
𝐴) |
21 | | iuneq1 4907 |
. . . . 5
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥)) |
22 | | 0iun 4958 |
. . . . 5
⊢ ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥) = ∅ |
23 | 21, 22 | eqtrdi 2790 |
. . . 4
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∅) |
24 | 20, 23 | eqeq12d 2755 |
. . 3
⊢ (𝐵 = ∅ → ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) ↔ 𝐴 = ∅)) |
25 | 24 | biimpcd 252 |
. 2
⊢ ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) → (𝐵 = ∅ → 𝐴 = ∅)) |
26 | 14, 25 | impbii 212 |
1
⊢ ((𝐵 = ∅ → 𝐴 = ∅) ↔ (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) |