Step | Hyp | Ref
| Expression |
1 | | df-nqqs 7263 |
. . . . 5
⊢
Q = ((N × N) /
~Q ) |
2 | 1 | eleq2i 2224 |
. . . 4
⊢ (𝑦 ∈ Q ↔
𝑦 ∈ ((N
× N) / ~Q
)) |
3 | | vex 2715 |
. . . . 5
⊢ 𝑦 ∈ V |
4 | 3 | elqs 6528 |
. . . 4
⊢ (𝑦 ∈ ((N
× N) / ~Q ) ↔
∃𝑥 ∈
(N × N)𝑦 = [𝑥] ~Q
) |
5 | | df-rex 2441 |
. . . 4
⊢
(∃𝑥 ∈
(N × N)𝑦 = [𝑥] ~Q ↔
∃𝑥(𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q )) |
6 | 2, 4, 5 | 3bitri 205 |
. . 3
⊢ (𝑦 ∈ Q ↔
∃𝑥(𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q )) |
7 | | elxpi 4601 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → ∃𝑢∃𝑣(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈
N))) |
8 | | nqnq0pi 7353 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ N ∧
𝑣 ∈ N)
→ [〈𝑢, 𝑣〉]
~Q0 = [〈𝑢, 𝑣〉] ~Q
) |
9 | 8 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
[〈𝑢, 𝑣〉]
~Q0 = [〈𝑢, 𝑣〉] ~Q
) |
10 | | eceq1 6512 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑢, 𝑣〉 → [𝑥] ~Q0 = [〈𝑢, 𝑣〉] ~Q0
) |
11 | | eceq1 6512 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑢, 𝑣〉 → [𝑥] ~Q = [〈𝑢, 𝑣〉] ~Q
) |
12 | 10, 11 | eqeq12d 2172 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝑢, 𝑣〉 → ([𝑥] ~Q0 = [𝑥] ~Q
↔ [〈𝑢, 𝑣〉]
~Q0 = [〈𝑢, 𝑣〉] ~Q
)) |
13 | 12 | adantr 274 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
([𝑥]
~Q0 = [𝑥] ~Q ↔
[〈𝑢, 𝑣〉]
~Q0 = [〈𝑢, 𝑣〉] ~Q
)) |
14 | 9, 13 | mpbird 166 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
[𝑥]
~Q0 = [𝑥] ~Q
) |
15 | | pinn 7224 |
. . . . . . . . . . . . 13
⊢ (𝑢 ∈ N →
𝑢 ∈
ω) |
16 | | opelxpi 4617 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ω ∧ 𝑣 ∈ N) →
〈𝑢, 𝑣〉 ∈ (ω ×
N)) |
17 | 15, 16 | sylan 281 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ N ∧
𝑣 ∈ N)
→ 〈𝑢, 𝑣〉 ∈ (ω ×
N)) |
18 | 17 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
〈𝑢, 𝑣〉 ∈ (ω ×
N)) |
19 | | eleq1 2220 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑢, 𝑣〉 → (𝑥 ∈ (ω × N)
↔ 〈𝑢, 𝑣〉 ∈ (ω ×
N))) |
20 | 19 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
(𝑥 ∈ (ω ×
N) ↔ 〈𝑢, 𝑣〉 ∈ (ω ×
N))) |
21 | 18, 20 | mpbird 166 |
. . . . . . . . . 10
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
𝑥 ∈ (ω ×
N)) |
22 | | enq0ex 7354 |
. . . . . . . . . . . 12
⊢
~Q0 ∈ V |
23 | 22 | ecelqsi 6531 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ω ×
N) → [𝑥]
~Q0 ∈ ((ω × N) /
~Q0 )) |
24 | | df-nq0 7340 |
. . . . . . . . . . 11
⊢
Q0 = ((ω × N)
/ ~Q0 ) |
25 | 23, 24 | eleqtrrdi 2251 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (ω ×
N) → [𝑥]
~Q0 ∈
Q0) |
26 | 21, 25 | syl 14 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
[𝑥]
~Q0 ∈
Q0) |
27 | 14, 26 | eqeltrrd 2235 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
[𝑥]
~Q ∈
Q0) |
28 | 27 | exlimivv 1876 |
. . . . . . 7
⊢
(∃𝑢∃𝑣(𝑥 = 〈𝑢, 𝑣〉 ∧ (𝑢 ∈ N ∧ 𝑣 ∈ N)) →
[𝑥]
~Q ∈
Q0) |
29 | 7, 28 | syl 14 |
. . . . . 6
⊢ (𝑥 ∈ (N ×
N) → [𝑥]
~Q ∈
Q0) |
30 | 29 | adantr 274 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q ) → [𝑥] ~Q ∈
Q0) |
31 | | eleq1 2220 |
. . . . . 6
⊢ (𝑦 = [𝑥] ~Q → (𝑦 ∈
Q0 ↔ [𝑥] ~Q ∈
Q0)) |
32 | 31 | adantl 275 |
. . . . 5
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q ) → (𝑦 ∈ Q0 ↔
[𝑥]
~Q ∈
Q0)) |
33 | 30, 32 | mpbird 166 |
. . . 4
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q ) → 𝑦 ∈
Q0) |
34 | 33 | exlimiv 1578 |
. . 3
⊢
(∃𝑥(𝑥 ∈ (N ×
N) ∧ 𝑦 =
[𝑥]
~Q ) → 𝑦 ∈
Q0) |
35 | 6, 34 | sylbi 120 |
. 2
⊢ (𝑦 ∈ Q →
𝑦 ∈
Q0) |
36 | 35 | ssriv 3132 |
1
⊢
Q ⊆ Q0 |