Proof of Theorem eliunxp2
Step | Hyp | Ref
| Expression |
1 | | relxp 5360 |
. . . . . . . 8
⊢ Rel
(𝐴 × {𝑦}) |
2 | 1 | rgenw 3133 |
. . . . . . 7
⊢
∀𝑦 ∈
𝐵 Rel (𝐴 × {𝑦}) |
3 | | reliun 5474 |
. . . . . . 7
⊢ (Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∀𝑦 ∈ 𝐵 Rel (𝐴 × {𝑦})) |
4 | 2, 3 | mpbir 223 |
. . . . . 6
⊢ Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
5 | | elrel 5456 |
. . . . . 6
⊢ ((Rel
∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
6 | 4, 5 | mpan 681 |
. . . . 5
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
7 | | excom 2212 |
. . . . 5
⊢
(∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ↔ ∃𝑥∃𝑦 𝐶 = 〈𝑥, 𝑦〉) |
8 | 6, 7 | sylibr 226 |
. . . 4
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) → ∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉) |
9 | 8 | pm4.71ri 556 |
. . 3
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
10 | | nfiu1 4770 |
. . . . 5
⊢
Ⅎ𝑦∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
11 | 10 | nfel2 2986 |
. . . 4
⊢
Ⅎ𝑦 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) |
12 | 11 | 19.41 2278 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑦∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
13 | | 19.41v 2048 |
. . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
14 | | eleq1 2894 |
. . . . . . . 8
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ 〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}))) |
15 | | opeliun2xp 42951 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴)) |
16 | | ancom 454 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
17 | 15, 16 | bitri 267 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
18 | 14, 17 | syl6bb 279 |
. . . . . . 7
⊢ (𝐶 = 〈𝑥, 𝑦〉 → (𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
19 | 18 | pm5.32i 570 |
. . . . . 6
⊢ ((𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ (𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
20 | 19 | exbii 1947 |
. . . . 5
⊢
(∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
21 | 13, 20 | bitr3i 269 |
. . . 4
⊢
((∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
22 | 21 | exbii 1947 |
. . 3
⊢
(∃𝑦(∃𝑥 𝐶 = 〈𝑥, 𝑦〉 ∧ 𝐶 ∈ ∪
𝑦 ∈ 𝐵 (𝐴 × {𝑦})) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
23 | 9, 12, 22 | 3bitr2i 291 |
. 2
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
24 | | excom 2212 |
. 2
⊢
(∃𝑦∃𝑥(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
25 | 23, 24 | bitri 267 |
1
⊢ (𝐶 ∈ ∪ 𝑦 ∈ 𝐵 (𝐴 × {𝑦}) ↔ ∃𝑥∃𝑦(𝐶 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |