Step | Hyp | Ref
| Expression |
1 | | elqsi 6600 |
. . 3
⊢ (𝑥 ∈ ((N
× N) / ~Q ) →
∃𝑎 ∈
(N × N)𝑥 = [𝑎] ~Q
) |
2 | | elxpi 4654 |
. . . . . . . 8
⊢ (𝑎 ∈ (N ×
N) → ∃𝑤∃𝑣(𝑎 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ N ∧ 𝑣 ∈
N))) |
3 | | simpl 109 |
. . . . . . . . 9
⊢ ((𝑎 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ N ∧ 𝑣 ∈ N)) →
𝑎 = ⟨𝑤, 𝑣⟩) |
4 | 3 | 2eximi 1611 |
. . . . . . . 8
⊢
(∃𝑤∃𝑣(𝑎 = ⟨𝑤, 𝑣⟩ ∧ (𝑤 ∈ N ∧ 𝑣 ∈ N)) →
∃𝑤∃𝑣 𝑎 = ⟨𝑤, 𝑣⟩) |
5 | 2, 4 | syl 14 |
. . . . . . 7
⊢ (𝑎 ∈ (N ×
N) → ∃𝑤∃𝑣 𝑎 = ⟨𝑤, 𝑣⟩) |
6 | 5 | anim1i 340 |
. . . . . 6
⊢ ((𝑎 ∈ (N ×
N) ∧ 𝑥 =
[𝑎]
~Q ) → (∃𝑤∃𝑣 𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q
)) |
7 | | 19.41vv 1913 |
. . . . . 6
⊢
(∃𝑤∃𝑣(𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q ) ↔
(∃𝑤∃𝑣 𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q
)) |
8 | 6, 7 | sylibr 134 |
. . . . 5
⊢ ((𝑎 ∈ (N ×
N) ∧ 𝑥 =
[𝑎]
~Q ) → ∃𝑤∃𝑣(𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q
)) |
9 | | simpr 110 |
. . . . . . 7
⊢ ((𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q ) → 𝑥 = [𝑎] ~Q
) |
10 | | eceq1 6583 |
. . . . . . . 8
⊢ (𝑎 = ⟨𝑤, 𝑣⟩ → [𝑎] ~Q = [⟨𝑤, 𝑣⟩] ~Q
) |
11 | 10 | adantr 276 |
. . . . . . 7
⊢ ((𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q ) → [𝑎] ~Q =
[⟨𝑤, 𝑣⟩]
~Q ) |
12 | 9, 11 | eqtrd 2220 |
. . . . . 6
⊢ ((𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q ) → 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
13 | 12 | 2eximi 1611 |
. . . . 5
⊢
(∃𝑤∃𝑣(𝑎 = ⟨𝑤, 𝑣⟩ ∧ 𝑥 = [𝑎] ~Q ) →
∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
14 | 8, 13 | syl 14 |
. . . 4
⊢ ((𝑎 ∈ (N ×
N) ∧ 𝑥 =
[𝑎]
~Q ) → ∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
15 | 14 | rexlimiva 2599 |
. . 3
⊢
(∃𝑎 ∈
(N × N)𝑥 = [𝑎] ~Q →
∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
16 | 1, 15 | syl 14 |
. 2
⊢ (𝑥 ∈ ((N
× N) / ~Q ) →
∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |
17 | | df-nqqs 7360 |
. 2
⊢
Q = ((N × N) /
~Q ) |
18 | 16, 17 | eleq2s 2282 |
1
⊢ (𝑥 ∈ Q →
∃𝑤∃𝑣 𝑥 = [⟨𝑤, 𝑣⟩] ~Q
) |