Proof of Theorem iununi
Step | Hyp | Ref
| Expression |
1 | | df-ne 3017 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔ ¬ 𝐵 = ∅) |
2 | | iunconst 4928 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
3 | 1, 2 | sylbir 237 |
. . . . . 6
⊢ (¬
𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
4 | | iun0 4985 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝐵 ∅ = ∅ |
5 | | id 22 |
. . . . . . . 8
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
6 | 5 | iuneq2d 4948 |
. . . . . . 7
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = ∪ 𝑥 ∈ 𝐵 ∅) |
7 | 4, 6, 5 | 3eqtr4a 2882 |
. . . . . 6
⊢ (𝐴 = ∅ → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
8 | 3, 7 | ja 188 |
. . . . 5
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → ∪ 𝑥 ∈ 𝐵 𝐴 = 𝐴) |
9 | 8 | eqcomd 2827 |
. . . 4
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → 𝐴 = ∪ 𝑥 ∈ 𝐵 𝐴) |
10 | 9 | uneq1d 4138 |
. . 3
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥)) |
11 | | uniiun 4982 |
. . . 4
⊢ ∪ 𝐵 =
∪ 𝑥 ∈ 𝐵 𝑥 |
12 | 11 | uneq2i 4136 |
. . 3
⊢ (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪ ∪ 𝑥 ∈ 𝐵 𝑥) |
13 | | iunun 5015 |
. . 3
⊢ ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = (∪
𝑥 ∈ 𝐵 𝐴 ∪ ∪
𝑥 ∈ 𝐵 𝑥) |
14 | 10, 12, 13 | 3eqtr4g 2881 |
. 2
⊢ ((𝐵 = ∅ → 𝐴 = ∅) → (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) |
15 | | unieq 4849 |
. . . . . . 7
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∪ ∅) |
16 | | uni0 4866 |
. . . . . . 7
⊢ ∪ ∅ = ∅ |
17 | 15, 16 | syl6eq 2872 |
. . . . . 6
⊢ (𝐵 = ∅ → ∪ 𝐵 =
∅) |
18 | 17 | uneq2d 4139 |
. . . . 5
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
(𝐴 ∪
∅)) |
19 | | un0 4344 |
. . . . 5
⊢ (𝐴 ∪ ∅) = 𝐴 |
20 | 18, 19 | syl6eq 2872 |
. . . 4
⊢ (𝐵 = ∅ → (𝐴 ∪ ∪ 𝐵) =
𝐴) |
21 | | iuneq1 4935 |
. . . . 5
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥)) |
22 | | 0iun 4986 |
. . . . 5
⊢ ∪ 𝑥 ∈ ∅ (𝐴 ∪ 𝑥) = ∅ |
23 | 21, 22 | syl6eq 2872 |
. . . 4
⊢ (𝐵 = ∅ → ∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) = ∅) |
24 | 20, 23 | eqeq12d 2837 |
. . 3
⊢ (𝐵 = ∅ → ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) ↔ 𝐴 = ∅)) |
25 | 24 | biimpcd 251 |
. 2
⊢ ((𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥) → (𝐵 = ∅ → 𝐴 = ∅)) |
26 | 14, 25 | impbii 211 |
1
⊢ ((𝐵 = ∅ → 𝐴 = ∅) ↔ (𝐴 ∪ ∪ 𝐵) =
∪ 𝑥 ∈ 𝐵 (𝐴 ∪ 𝑥)) |