Step | Hyp | Ref
| Expression |
1 | | df-nqqs 6332 |
. . . . 5
⊢
Q = ((N × N) /
~Q ) |
2 | 1 | eleq2i 2101 |
. . . 4
⊢ (y ∈
Q ↔ y ∈ ((N × N)
/ ~Q )) |
3 | | vex 2554 |
. . . . 5
⊢ y ∈
V |
4 | 3 | elqs 6093 |
. . . 4
⊢ (y ∈
((N × N) / ~Q
) ↔ ∃x ∈
(N × N)y
= [x] ~Q
) |
5 | | df-rex 2306 |
. . . 4
⊢ (∃x ∈ (N × N)y = [x]
~Q ↔ ∃x(x ∈ (N × N) ∧ y = [x] ~Q )) |
6 | 2, 4, 5 | 3bitri 195 |
. . 3
⊢ (y ∈
Q ↔ ∃x(x ∈ (N × N) ∧ y = [x] ~Q )) |
7 | | elxpi 4304 |
. . . . . . 7
⊢ (x ∈
(N × N) → ∃u∃v(x = 〈u,
v〉 ∧
(u ∈
N ∧ v ∈
N))) |
8 | | nqnq0pi 6421 |
. . . . . . . . . . 11
⊢
((u ∈ N ∧ v ∈ N) → [〈u, v〉]
~Q0 = [〈u,
v〉] ~Q
) |
9 | 8 | adantl 262 |
. . . . . . . . . 10
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → [〈u, v〉]
~Q0 = [〈u,
v〉] ~Q
) |
10 | | eceq1 6077 |
. . . . . . . . . . . 12
⊢ (x = 〈u,
v〉 → [x] ~Q0 = [〈u, v〉]
~Q0 ) |
11 | | eceq1 6077 |
. . . . . . . . . . . 12
⊢ (x = 〈u,
v〉 → [x] ~Q = [〈u, v〉]
~Q ) |
12 | 10, 11 | eqeq12d 2051 |
. . . . . . . . . . 11
⊢ (x = 〈u,
v〉 → ([x] ~Q0 = [x] ~Q ↔
[〈u, v〉] ~Q0 =
[〈u, v〉] ~Q
)) |
13 | 12 | adantr 261 |
. . . . . . . . . 10
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → ([x] ~Q0 = [x] ~Q ↔
[〈u, v〉] ~Q0 =
[〈u, v〉] ~Q
)) |
14 | 9, 13 | mpbird 156 |
. . . . . . . . 9
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → [x] ~Q0 = [x] ~Q ) |
15 | | pinn 6293 |
. . . . . . . . . . . . 13
⊢ (u ∈
N → u ∈ 𝜔) |
16 | | opelxpi 4319 |
. . . . . . . . . . . . 13
⊢
((u ∈ 𝜔 ∧
v ∈
N) → 〈u, v〉 ∈
(𝜔 × N)) |
17 | 15, 16 | sylan 267 |
. . . . . . . . . . . 12
⊢
((u ∈ N ∧ v ∈ N) → 〈u, v〉 ∈ (𝜔 ×
N)) |
18 | 17 | adantl 262 |
. . . . . . . . . . 11
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → 〈u, v〉 ∈ (𝜔 ×
N)) |
19 | | eleq1 2097 |
. . . . . . . . . . . 12
⊢ (x = 〈u,
v〉 → (x ∈ (𝜔
× N) ↔ 〈u,
v〉 ∈
(𝜔 × N))) |
20 | 19 | adantr 261 |
. . . . . . . . . . 11
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → (x ∈ (𝜔
× N) ↔ 〈u,
v〉 ∈
(𝜔 × N))) |
21 | 18, 20 | mpbird 156 |
. . . . . . . . . 10
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → x ∈ (𝜔
× N)) |
22 | | enq0ex 6422 |
. . . . . . . . . . . 12
⊢
~Q0 ∈
V |
23 | 22 | ecelqsi 6096 |
. . . . . . . . . . 11
⊢ (x ∈ (𝜔
× N) → [x]
~Q0 ∈ ((𝜔
× N) / ~Q0
)) |
24 | | df-nq0 6408 |
. . . . . . . . . . 11
⊢
Q0 = ((𝜔 × N)
/ ~Q0 ) |
25 | 23, 24 | syl6eleqr 2128 |
. . . . . . . . . 10
⊢ (x ∈ (𝜔
× N) → [x]
~Q0 ∈
Q0) |
26 | 21, 25 | syl 14 |
. . . . . . . . 9
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → [x] ~Q0 ∈ Q0) |
27 | 14, 26 | eqeltrrd 2112 |
. . . . . . . 8
⊢
((x = 〈u, v〉 ∧ (u ∈ N ∧ v ∈ N)) → [x] ~Q ∈ Q0) |
28 | 27 | exlimivv 1773 |
. . . . . . 7
⊢ (∃u∃v(x = 〈u,
v〉 ∧
(u ∈
N ∧ v ∈
N)) → [x]
~Q ∈
Q0) |
29 | 7, 28 | syl 14 |
. . . . . 6
⊢ (x ∈
(N × N) → [x] ~Q ∈ Q0) |
30 | 29 | adantr 261 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y = [x] ~Q ) → [x] ~Q ∈ Q0) |
31 | | eleq1 2097 |
. . . . . 6
⊢ (y = [x]
~Q → (y ∈ Q0 ↔ [x] ~Q ∈ Q0)) |
32 | 31 | adantl 262 |
. . . . 5
⊢
((x ∈ (N × N) ∧ y = [x] ~Q ) → (y ∈
Q0 ↔ [x]
~Q ∈
Q0)) |
33 | 30, 32 | mpbird 156 |
. . . 4
⊢
((x ∈ (N × N) ∧ y = [x] ~Q ) → y ∈
Q0) |
34 | 33 | exlimiv 1486 |
. . 3
⊢ (∃x(x ∈
(N × N) ∧
y = [x]
~Q ) → y
∈
Q0) |
35 | 6, 34 | sylbi 114 |
. 2
⊢ (y ∈
Q → y ∈ Q0) |
36 | 35 | ssriv 2943 |
1
⊢
Q ⊆ Q0 |