Proof of Theorem eliuniin2
| Step | Hyp | Ref
| Expression |
| 1 | | eliuniin2.2 |
. . . . 5
⊢ 𝐴 = ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 |
| 2 | 1 | eleq2i 2833 |
. . . 4
⊢ (𝑍 ∈ 𝐴 ↔ 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
| 3 | | eliun 4995 |
. . . 4
⊢ (𝑍 ∈ ∪ 𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
| 4 | 2, 3 | sylbb 219 |
. . 3
⊢ (𝑍 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
| 5 | | eliin 4996 |
. . . . . 6
⊢ (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
| 6 | 5 | ibi 267 |
. . . . 5
⊢ (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
| 7 | 6 | a1i 11 |
. . . 4
⊢ (𝑍 ∈ 𝐴 → (𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 → ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
| 8 | 7 | reximdv 3170 |
. . 3
⊢ (𝑍 ∈ 𝐴 → (∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
| 9 | 4, 8 | mpd 15 |
. 2
⊢ (𝑍 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) |
| 10 | | eliuniin2.1 |
. . . 4
⊢
Ⅎ𝑥𝐶 |
| 11 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑥∅ |
| 12 | 10, 11 | nfne 3043 |
. . 3
⊢
Ⅎ𝑥 𝐶 ≠ ∅ |
| 13 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥 𝑍 ∈ 𝐴 |
| 14 | | simp2 1138 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑥 ∈ 𝐵) |
| 15 | | eliin2 45121 |
. . . . . . . 8
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ ∩ 𝑦 ∈ 𝐶 𝐷 ↔ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |
| 16 | 15 | biimpar 477 |
. . . . . . 7
⊢ ((𝐶 ≠ ∅ ∧
∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
| 17 | | rspe 3249 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
| 18 | 14, 16, 17 | 3imp3i2an 1346 |
. . . . . 6
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → ∃𝑥 ∈ 𝐵 𝑍 ∈ ∩
𝑦 ∈ 𝐶 𝐷) |
| 19 | 18, 3 | sylibr 234 |
. . . . 5
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ ∪
𝑥 ∈ 𝐵 ∩ 𝑦 ∈ 𝐶 𝐷) |
| 20 | 19, 2 | sylibr 234 |
. . . 4
⊢ ((𝐶 ≠ ∅ ∧ 𝑥 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷) → 𝑍 ∈ 𝐴) |
| 21 | 20 | 3exp 1120 |
. . 3
⊢ (𝐶 ≠ ∅ → (𝑥 ∈ 𝐵 → (∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴))) |
| 22 | 12, 13, 21 | rexlimd 3266 |
. 2
⊢ (𝐶 ≠ ∅ →
(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷 → 𝑍 ∈ 𝐴)) |
| 23 | 9, 22 | impbid2 226 |
1
⊢ (𝐶 ≠ ∅ → (𝑍 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐶 𝑍 ∈ 𝐷)) |