Step | Hyp | Ref
| Expression |
1 | | elqsi 6534 |
. . 3
⊢ (𝐴 ∈ ((ω ×
N) / ~Q0 ) → ∃𝑎 ∈ (ω ×
N)𝐴 = [𝑎] ~Q0
) |
2 | | elxpi 4604 |
. . . . . . 7
⊢ (𝑎 ∈ (ω ×
N) → ∃𝑤∃𝑣(𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N))) |
3 | 2 | anim1i 338 |
. . . . . 6
⊢ ((𝑎 ∈ (ω ×
N) ∧ 𝐴 =
[𝑎]
~Q0 ) → (∃𝑤∃𝑣(𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0
)) |
4 | | 19.41vv 1883 |
. . . . . 6
⊢
(∃𝑤∃𝑣((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) ↔
(∃𝑤∃𝑣(𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0
)) |
5 | 3, 4 | sylibr 133 |
. . . . 5
⊢ ((𝑎 ∈ (ω ×
N) ∧ 𝐴 =
[𝑎]
~Q0 ) → ∃𝑤∃𝑣((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0
)) |
6 | | simplr 520 |
. . . . . . 7
⊢ (((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) →
(𝑤 ∈ ω ∧
𝑣 ∈
N)) |
7 | | simpr 109 |
. . . . . . . 8
⊢ (((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) → 𝐴 = [𝑎] ~Q0
) |
8 | | eceq1 6517 |
. . . . . . . . 9
⊢ (𝑎 = 〈𝑤, 𝑣〉 → [𝑎] ~Q0 = [〈𝑤, 𝑣〉] ~Q0
) |
9 | 8 | ad2antrr 480 |
. . . . . . . 8
⊢ (((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) →
[𝑎]
~Q0 = [〈𝑤, 𝑣〉] ~Q0
) |
10 | 7, 9 | eqtrd 2190 |
. . . . . . 7
⊢ (((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) → 𝐴 = [〈𝑤, 𝑣〉] ~Q0
) |
11 | 6, 10 | jca 304 |
. . . . . 6
⊢ (((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) →
((𝑤 ∈ ω ∧
𝑣 ∈ N)
∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
12 | 11 | 2eximi 1581 |
. . . . 5
⊢
(∃𝑤∃𝑣((𝑎 = 〈𝑤, 𝑣〉 ∧ (𝑤 ∈ ω ∧ 𝑣 ∈ N)) ∧ 𝐴 = [𝑎] ~Q0 ) →
∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
13 | 5, 12 | syl 14 |
. . . 4
⊢ ((𝑎 ∈ (ω ×
N) ∧ 𝐴 =
[𝑎]
~Q0 ) → ∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
14 | 13 | rexlimiva 2569 |
. . 3
⊢
(∃𝑎 ∈
(ω × N)𝐴 = [𝑎] ~Q0 →
∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
15 | 1, 14 | syl 14 |
. 2
⊢ (𝐴 ∈ ((ω ×
N) / ~Q0 ) → ∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |
16 | | df-nq0 7347 |
. 2
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
17 | 15, 16 | eleq2s 2252 |
1
⊢ (𝐴 ∈
Q0 → ∃𝑤∃𝑣((𝑤 ∈ ω ∧ 𝑣 ∈ N) ∧ 𝐴 = [〈𝑤, 𝑣〉] ~Q0
)) |