Step | Hyp | Ref
| Expression |
1 | | elxp 5131 |
. . . 4
⊢ (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
2 | | df-rex 2918 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
3 | | an13 840 |
. . . . . . . . 9
⊢ ((𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
4 | 3 | exbii 1774 |
. . . . . . . 8
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
5 | 2, 4 | bitr4i 267 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
6 | | velsn 4193 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋) |
7 | 6 | anbi1i 731 |
. . . . . . . . 9
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ (𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉)) |
8 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑥, 𝑦〉) |
9 | | opeq1 4402 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
10 | 9 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
11 | 8, 10 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
12 | 7, 11 | sylbi 207 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
13 | 12 | reximi 3011 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
14 | 5, 13 | sylbir 225 |
. . . . . 6
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
15 | 14 | eximi 1762 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑥∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
16 | | 19.9v 1896 |
. . . . 5
⊢
(∃𝑥∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
17 | 15, 16 | sylib 208 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
18 | 1, 17 | sylbi 207 |
. . 3
⊢ (𝑍 ∈ ({𝑋} × 𝐴) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
19 | 18 | adantl 482 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ ({𝑋} × 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
20 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑦 𝑋 ∈ 𝑉 |
21 | | nfre1 3005 |
. . . 4
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 |
22 | 20, 21 | nfan 1828 |
. . 3
⊢
Ⅎ𝑦(𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
23 | | simpr 477 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
24 | | snidg 4206 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
25 | 24 | adantr 481 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 𝑋 ∈ {𝑋}) |
26 | | simpr 477 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
27 | | opelxp 5146 |
. . . . . . . 8
⊢
(〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴) ↔ (𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) |
28 | 27 | biimpri 218 |
. . . . . . 7
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
29 | 25, 26, 28 | syl2anc 693 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
30 | 29 | adantr 481 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
31 | 23, 30 | eqeltrd 2701 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
32 | 31 | adantllr 755 |
. . 3
⊢ ((((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
33 | | simpr 477 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
34 | 22, 32, 33 | r19.29af 3076 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
35 | 19, 34 | impbida 877 |
1
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) |