Step | Hyp | Ref
| Expression |
1 | | elxp 5055 |
. . . 4
⊢ (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
2 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
3 | | an13 836 |
. . . . . . . . 9
⊢ ((𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
4 | 3 | exbii 1764 |
. . . . . . . 8
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉))) |
5 | 2, 4 | bitr4i 266 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ ∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴))) |
6 | | velsn 4141 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝑋} ↔ 𝑥 = 𝑋) |
7 | 6 | anbi1i 727 |
. . . . . . . . 9
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) ↔ (𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉)) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑥, 𝑦〉) |
9 | | opeq1 4340 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 〈𝑥, 𝑦〉 = 〈𝑋, 𝑦〉) |
11 | 8, 10 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑋 ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
12 | 7, 11 | sylbi 206 |
. . . . . . . 8
⊢ ((𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
13 | 12 | reximi 2994 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐴 (𝑥 ∈ {𝑋} ∧ 𝑍 = 〈𝑥, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
14 | 5, 13 | sylbir 224 |
. . . . . 6
⊢
(∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
15 | 14 | eximi 1752 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑥∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
16 | | 19.9v 1883 |
. . . . 5
⊢
(∃𝑥∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
17 | 15, 16 | sylib 207 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑍 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
18 | 1, 17 | sylbi 206 |
. . 3
⊢ (𝑍 ∈ ({𝑋} × 𝐴) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
19 | 18 | adantl 481 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑍 ∈ ({𝑋} × 𝐴)) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
20 | | nfv 1830 |
. . . 4
⊢
Ⅎ𝑦 𝑋 ∈ 𝑉 |
21 | | nfre1 2988 |
. . . 4
⊢
Ⅎ𝑦∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉 |
22 | 20, 21 | nfan 1816 |
. . 3
⊢
Ⅎ𝑦(𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
23 | | simpr 476 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 = 〈𝑋, 𝑦〉) |
24 | | snidg 4153 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 𝑋 ∈ {𝑋}) |
26 | | simpr 476 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
27 | | opelxp 5070 |
. . . . . . . 8
⊢
(〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴) ↔ (𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴)) |
28 | 27 | biimpri 217 |
. . . . . . 7
⊢ ((𝑋 ∈ {𝑋} ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
29 | 25, 26, 28 | syl2anc 691 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
30 | 29 | adantr 480 |
. . . . 5
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 〈𝑋, 𝑦〉 ∈ ({𝑋} × 𝐴)) |
31 | 23, 30 | eqeltrd 2688 |
. . . 4
⊢ (((𝑋 ∈ 𝑉 ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
32 | 31 | adantllr 751 |
. . 3
⊢ ((((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) ∧ 𝑦 ∈ 𝐴) ∧ 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
33 | | simpr 476 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) → ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) |
34 | 22, 32, 33 | r19.29af 3058 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉) → 𝑍 ∈ ({𝑋} × 𝐴)) |
35 | 19, 34 | impbida 873 |
1
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) |