Step | Hyp | Ref
| Expression |
1 | | df-erq 9735 |
. . . . . . 7
⊢
[Q] = ( ~Q ∩
((N × N) ×
Q)) |
2 | | inss2 3834 |
. . . . . . 7
⊢ (
~Q ∩ ((N × N)
× Q)) ⊆ ((N × N)
× Q) |
3 | 1, 2 | eqsstri 3635 |
. . . . . 6
⊢
[Q] ⊆ ((N × N)
× Q) |
4 | | xpss 5226 |
. . . . . 6
⊢
((N × N) × Q)
⊆ (V × V) |
5 | 3, 4 | sstri 3612 |
. . . . 5
⊢
[Q] ⊆ (V × V) |
6 | | df-rel 5121 |
. . . . 5
⊢ (Rel
[Q] ↔ [Q] ⊆ (V ×
V)) |
7 | 5, 6 | mpbir 221 |
. . . 4
⊢ Rel
[Q] |
8 | | nqereu 9751 |
. . . . . . . 8
⊢ (𝑥 ∈ (N ×
N) → ∃!𝑦 ∈ Q 𝑦 ~Q 𝑥) |
9 | | df-reu 2919 |
. . . . . . . . 9
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 ↔ ∃!𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
10 | | eumo 2499 |
. . . . . . . . 9
⊢
(∃!𝑦(𝑦 ∈ Q ∧
𝑦
~Q 𝑥) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
11 | 9, 10 | sylbi 207 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
12 | 8, 11 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
13 | | moanimv 2531 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) ↔ (𝑥 ∈ (N ×
N) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥))) |
14 | 12, 13 | mpbir 221 |
. . . . . 6
⊢
∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) |
15 | 3 | brel 5168 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 → (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q)) |
16 | 15 | simpld 475 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑥 ∈ (N ×
N)) |
17 | 15 | simprd 479 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑦 ∈ Q) |
18 | | enqer 9743 |
. . . . . . . . . 10
⊢
~Q Er (N ×
N) |
19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 →
~Q Er (N ×
N)) |
20 | | inss1 3833 |
. . . . . . . . . . 11
⊢ (
~Q ∩ ((N × N)
× Q)) ⊆ ~Q |
21 | 1, 20 | eqsstri 3635 |
. . . . . . . . . 10
⊢
[Q] ⊆ ~Q |
22 | 21 | ssbri 4697 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 → 𝑥 ~Q 𝑦) |
23 | 19, 22 | ersym 7754 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑦 ~Q 𝑥) |
24 | 16, 17, 23 | jca32 558 |
. . . . . . 7
⊢ (𝑥[Q]𝑦 → (𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥))) |
25 | 24 | moimi 2520 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) → ∃*𝑦 𝑥[Q]𝑦) |
26 | 14, 25 | ax-mp 5 |
. . . . 5
⊢
∃*𝑦 𝑥[Q]𝑦 |
27 | 26 | ax-gen 1722 |
. . . 4
⊢
∀𝑥∃*𝑦 𝑥[Q]𝑦 |
28 | | dffun6 5903 |
. . . 4
⊢ (Fun
[Q] ↔ (Rel [Q] ∧ ∀𝑥∃*𝑦 𝑥[Q]𝑦)) |
29 | 7, 27, 28 | mpbir2an 955 |
. . 3
⊢ Fun
[Q] |
30 | | dmss 5323 |
. . . . . 6
⊢
([Q] ⊆ ((N × N)
× Q) → dom [Q] ⊆ dom
((N × N) ×
Q)) |
31 | 3, 30 | ax-mp 5 |
. . . . 5
⊢ dom
[Q] ⊆ dom ((N × N)
× Q) |
32 | | 1nq 9750 |
. . . . . 6
⊢
1Q ∈ Q |
33 | | ne0i 3921 |
. . . . . 6
⊢
(1Q ∈ Q →
Q ≠ ∅) |
34 | | dmxp 5344 |
. . . . . 6
⊢
(Q ≠ ∅ → dom ((N ×
N) × Q) = (N ×
N)) |
35 | 32, 33, 34 | mp2b 10 |
. . . . 5
⊢ dom
((N × N) × Q) =
(N × N) |
36 | 31, 35 | sseqtri 3637 |
. . . 4
⊢ dom
[Q] ⊆ (N ×
N) |
37 | | reurex 3160 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 → ∃𝑦 ∈ Q 𝑦 ~Q 𝑥) |
38 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥 ∈ (N ×
N)) |
39 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑦 ∈ Q) |
40 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) →
~Q Er (N ×
N)) |
41 | | simpr 477 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑦 ~Q 𝑥) |
42 | 40, 41 | ersym 7754 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥 ~Q 𝑦) |
43 | 1 | breqi 4659 |
. . . . . . . . . . . 12
⊢ (𝑥[Q]𝑦 ↔ 𝑥( ~Q ∩
((N × N) × Q))𝑦) |
44 | | brinxp2 5180 |
. . . . . . . . . . . 12
⊢ (𝑥( ~Q
∩ ((N × N) × Q))𝑦 ↔ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q ∧ 𝑥 ~Q 𝑦)) |
45 | 43, 44 | bitri 264 |
. . . . . . . . . . 11
⊢ (𝑥[Q]𝑦 ↔ (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q ∧ 𝑥 ~Q 𝑦)) |
46 | 38, 39, 42, 45 | syl3anbrc 1246 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥[Q]𝑦) |
47 | 46 | ex 450 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) → (𝑦 ~Q 𝑥 → 𝑥[Q]𝑦)) |
48 | 47 | reximdva 3017 |
. . . . . . . 8
⊢ (𝑥 ∈ (N ×
N) → (∃𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃𝑦 ∈ Q 𝑥[Q]𝑦)) |
49 | | rexex 3002 |
. . . . . . . 8
⊢
(∃𝑦 ∈
Q 𝑥[Q]𝑦 → ∃𝑦 𝑥[Q]𝑦) |
50 | 37, 48, 49 | syl56 36 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → (∃!𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃𝑦 𝑥[Q]𝑦)) |
51 | 8, 50 | mpd 15 |
. . . . . 6
⊢ (𝑥 ∈ (N ×
N) → ∃𝑦 𝑥[Q]𝑦) |
52 | | vex 3203 |
. . . . . . 7
⊢ 𝑥 ∈ V |
53 | 52 | eldm 5321 |
. . . . . 6
⊢ (𝑥 ∈ dom [Q]
↔ ∃𝑦 𝑥[Q]𝑦) |
54 | 51, 53 | sylibr 224 |
. . . . 5
⊢ (𝑥 ∈ (N ×
N) → 𝑥
∈ dom [Q]) |
55 | 54 | ssriv 3607 |
. . . 4
⊢
(N × N) ⊆ dom
[Q] |
56 | 36, 55 | eqssi 3619 |
. . 3
⊢ dom
[Q] = (N × N) |
57 | | df-fn 5891 |
. . 3
⊢
([Q] Fn (N × N) ↔
(Fun [Q] ∧ dom [Q] = (N ×
N))) |
58 | 29, 56, 57 | mpbir2an 955 |
. 2
⊢
[Q] Fn (N ×
N) |
59 | | rnss 5354 |
. . . 4
⊢
([Q] ⊆ ((N × N)
× Q) → ran [Q] ⊆ ran
((N × N) ×
Q)) |
60 | 3, 59 | ax-mp 5 |
. . 3
⊢ ran
[Q] ⊆ ran ((N × N)
× Q) |
61 | | rnxpss 5566 |
. . 3
⊢ ran
((N × N) × Q) ⊆
Q |
62 | 60, 61 | sstri 3612 |
. 2
⊢ ran
[Q] ⊆ Q |
63 | | df-f 5892 |
. 2
⊢
([Q]:(N ×
N)⟶Q ↔ ([Q] Fn
(N × N) ∧ ran [Q] ⊆
Q)) |
64 | 58, 62, 63 | mpbir2an 955 |
1
⊢
[Q]:(N ×
N)⟶Q |