| Step | Hyp | Ref
| Expression |
| 1 | | df-erq 10953 |
. . . . . . 7
⊢
[Q] = ( ~Q ∩
((N × N) ×
Q)) |
| 2 | | inss2 4238 |
. . . . . . 7
⊢ (
~Q ∩ ((N × N)
× Q)) ⊆ ((N × N)
× Q) |
| 3 | 1, 2 | eqsstri 4030 |
. . . . . 6
⊢
[Q] ⊆ ((N × N)
× Q) |
| 4 | | xpss 5701 |
. . . . . 6
⊢
((N × N) × Q)
⊆ (V × V) |
| 5 | 3, 4 | sstri 3993 |
. . . . 5
⊢
[Q] ⊆ (V × V) |
| 6 | | df-rel 5692 |
. . . . 5
⊢ (Rel
[Q] ↔ [Q] ⊆ (V ×
V)) |
| 7 | 5, 6 | mpbir 231 |
. . . 4
⊢ Rel
[Q] |
| 8 | | nqereu 10969 |
. . . . . . . 8
⊢ (𝑥 ∈ (N ×
N) → ∃!𝑦 ∈ Q 𝑦 ~Q 𝑥) |
| 9 | | df-reu 3381 |
. . . . . . . . 9
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 ↔ ∃!𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
| 10 | | eumo 2578 |
. . . . . . . . 9
⊢
(∃!𝑦(𝑦 ∈ Q ∧
𝑦
~Q 𝑥) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
| 11 | 9, 10 | sylbi 217 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
| 12 | 8, 11 | syl 17 |
. . . . . . 7
⊢ (𝑥 ∈ (N ×
N) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥)) |
| 13 | | moanimv 2619 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) ↔ (𝑥 ∈ (N ×
N) → ∃*𝑦(𝑦 ∈ Q ∧ 𝑦 ~Q
𝑥))) |
| 14 | 12, 13 | mpbir 231 |
. . . . . 6
⊢
∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) |
| 15 | 3 | brel 5750 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 → (𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q)) |
| 16 | 15 | simpld 494 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑥 ∈ (N ×
N)) |
| 17 | 15 | simprd 495 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑦 ∈ Q) |
| 18 | | enqer 10961 |
. . . . . . . . . 10
⊢
~Q Er (N ×
N) |
| 19 | 18 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 →
~Q Er (N ×
N)) |
| 20 | | inss1 4237 |
. . . . . . . . . . 11
⊢ (
~Q ∩ ((N × N)
× Q)) ⊆ ~Q |
| 21 | 1, 20 | eqsstri 4030 |
. . . . . . . . . 10
⊢
[Q] ⊆ ~Q |
| 22 | 21 | ssbri 5188 |
. . . . . . . . 9
⊢ (𝑥[Q]𝑦 → 𝑥 ~Q 𝑦) |
| 23 | 19, 22 | ersym 8757 |
. . . . . . . 8
⊢ (𝑥[Q]𝑦 → 𝑦 ~Q 𝑥) |
| 24 | 16, 17, 23 | jca32 515 |
. . . . . . 7
⊢ (𝑥[Q]𝑦 → (𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥))) |
| 25 | 24 | moimi 2545 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ (N ×
N) ∧ (𝑦
∈ Q ∧ 𝑦 ~Q 𝑥)) → ∃*𝑦 𝑥[Q]𝑦) |
| 26 | 14, 25 | ax-mp 5 |
. . . . 5
⊢
∃*𝑦 𝑥[Q]𝑦 |
| 27 | 26 | ax-gen 1795 |
. . . 4
⊢
∀𝑥∃*𝑦 𝑥[Q]𝑦 |
| 28 | | dffun6 6574 |
. . . 4
⊢ (Fun
[Q] ↔ (Rel [Q] ∧ ∀𝑥∃*𝑦 𝑥[Q]𝑦)) |
| 29 | 7, 27, 28 | mpbir2an 711 |
. . 3
⊢ Fun
[Q] |
| 30 | | dmss 5913 |
. . . . . 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 10968 |
. . . . . 6
⊢
1Q ∈ Q |
| 33 | | ne0i 4341 |
. . . . . 6
⊢
(1Q ∈ Q →
Q ≠ ∅) |
| 34 | | dmxp 5939 |
. . . . . 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 4032 |
. . . 4
⊢ dom
[Q] ⊆ (N ×
N) |
| 37 | | reurex 3384 |
. . . . . . . 8
⊢
(∃!𝑦 ∈
Q 𝑦
~Q 𝑥 → ∃𝑦 ∈ Q 𝑦 ~Q 𝑥) |
| 38 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥 ∈ (N ×
N)) |
| 39 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑦 ∈ Q) |
| 40 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) →
~Q Er (N ×
N)) |
| 41 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑦 ~Q 𝑥) |
| 42 | 40, 41 | ersym 8757 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥 ~Q 𝑦) |
| 43 | 1 | breqi 5149 |
. . . . . . . . . . . 12
⊢ (𝑥[Q]𝑦 ↔ 𝑥( ~Q ∩
((N × N) × Q))𝑦) |
| 44 | | brinxp2 5763 |
. . . . . . . . . . . 12
⊢ (𝑥( ~Q
∩ ((N × N) × Q))𝑦 ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑥 ~Q 𝑦)) |
| 45 | 43, 44 | bitri 275 |
. . . . . . . . . . 11
⊢ (𝑥[Q]𝑦 ↔ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑥 ~Q 𝑦)) |
| 46 | 38, 39, 42, 45 | syl21anbrc 1345 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) ∧ 𝑦 ~Q 𝑥) → 𝑥[Q]𝑦) |
| 47 | 46 | ex 412 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (N ×
N) ∧ 𝑦
∈ Q) → (𝑦 ~Q 𝑥 → 𝑥[Q]𝑦)) |
| 48 | 47 | reximdva 3168 |
. . . . . . . 8
⊢ (𝑥 ∈ (N ×
N) → (∃𝑦 ∈ Q 𝑦 ~Q 𝑥 → ∃𝑦 ∈ Q 𝑥[Q]𝑦)) |
| 49 | | rexex 3076 |
. . . . . . . 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 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 53 | 52 | eldm 5911 |
. . . . . 6
⊢ (𝑥 ∈ dom [Q]
↔ ∃𝑦 𝑥[Q]𝑦) |
| 54 | 51, 53 | sylibr 234 |
. . . . 5
⊢ (𝑥 ∈ (N ×
N) → 𝑥
∈ dom [Q]) |
| 55 | 54 | ssriv 3987 |
. . . 4
⊢
(N × N) ⊆ dom
[Q] |
| 56 | 36, 55 | eqssi 4000 |
. . 3
⊢ dom
[Q] = (N × N) |
| 57 | | df-fn 6564 |
. . 3
⊢
([Q] Fn (N × N) ↔
(Fun [Q] ∧ dom [Q] = (N ×
N))) |
| 58 | 29, 56, 57 | mpbir2an 711 |
. 2
⊢
[Q] Fn (N ×
N) |
| 59 | 3 | rnssi 5951 |
. . 3
⊢ ran
[Q] ⊆ ran ((N × N)
× Q) |
| 60 | | rnxpss 6192 |
. . 3
⊢ ran
((N × N) × Q) ⊆
Q |
| 61 | 59, 60 | sstri 3993 |
. 2
⊢ ran
[Q] ⊆ Q |
| 62 | | df-f 6565 |
. 2
⊢
([Q]:(N ×
N)⟶Q ↔ ([Q] Fn
(N × N) ∧ ran [Q] ⊆
Q)) |
| 63 | 58, 61, 62 | mpbir2an 711 |
1
⊢
[Q]:(N ×
N)⟶Q |