Proof of Theorem eliunxp
| Step | Hyp | Ref
| Expression |
| 1 | | relxp 5703 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐵) |
| 2 | 1 | rgenw 3065 |
. . . . 5
⊢
∀𝑥 ∈
𝐴 Rel ({𝑥} × 𝐵) |
| 3 | | reliun 5826 |
. . . . 5
⊢ (Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∀𝑥 ∈ 𝐴 Rel ({𝑥} × 𝐵)) |
| 4 | 2, 3 | mpbir 231 |
. . . 4
⊢ Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
| 5 | | elrel 5808 |
. . . 4
⊢ ((Rel
∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
| 6 | 4, 5 | mpan 690 |
. . 3
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
| 7 | 6 | pm4.71ri 560 |
. 2
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
| 8 | | nfiu1 5027 |
. . . 4
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
| 9 | 8 | nfel2 2924 |
. . 3
⊢
Ⅎ𝑥 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
| 10 | 9 | 19.41 2235 |
. 2
⊢
(∃𝑥(∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ (∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
| 11 | | 19.41v 1949 |
. . . 4
⊢
(∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ (∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
| 12 | | eleq1 2829 |
. . . . . . 7
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
| 13 | | opeliunxp 5752 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 14 | 12, 13 | bitrdi 287 |
. . . . . 6
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 15 | 14 | pm5.32i 574 |
. . . . 5
⊢ ((𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ (𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 16 | 15 | exbii 1848 |
. . . 4
⊢
(∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ ∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 17 | 11, 16 | bitr3i 277 |
. . 3
⊢
((∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ ∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 18 | 17 | exbii 1848 |
. 2
⊢
(∃𝑥(∃𝑦 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 19 | 7, 10, 18 | 3bitr2i 299 |
1
⊢ (𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |