Proof of Theorem eliunxp2
Step | Hyp | Ref
| Expression |
1 | | relxp 5607 |
. . . . . . . 8
⊢ Rel
(𝐴 × {𝑦}) |
2 | 1 | rgenw 3076 |
. . . . . . 7
⊢
∀𝑦 ∈
𝐵 Rel (𝐴 × {𝑦}) |
3 | | reliun 5726 |
. . . . . . 7
⊢ (Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∀𝑦 ∈ 𝐵 Rel (𝐴 × {𝑦})) |
4 | 2, 3 | mpbir 230 |
. . . . . 6
⊢ Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
5 | | elrel 5708 |
. . . . . 6
⊢ ((Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
6 | 4, 5 | mpan 687 |
. . . . 5
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
7 | | excom 2162 |
. . . . 5
⊢
(∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
8 | 6, 7 | sylibr 233 |
. . . 4
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉) |
9 | 8 | pm4.71ri 561 |
. . 3
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
10 | | nfiu1 4958 |
. . . . 5
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
11 | 10 | nfel2 2925 |
. . . 4
⊢
Ⅎ𝑦 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
12 | 11 | 19.41 2228 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
13 | | 19.41v 1953 |
. . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
14 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
15 | | opeliun2xp 45668 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
16 | 15 | biancomi 463 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
17 | 14, 16 | bitrdi 287 |
. . . . . . 7
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
18 | 17 | pm5.32i 575 |
. . . . . 6
⊢ ((𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
19 | 18 | exbii 1850 |
. . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
20 | 13, 19 | bitr3i 276 |
. . . 4
⊢
((∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
21 | 20 | exbii 1850 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
22 | 9, 12, 21 | 3bitr2i 299 |
. 2
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
23 | | excom 2162 |
. 2
⊢
(∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
24 | 22, 23 | bitri 274 |
1
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |