Step | Hyp | Ref
| Expression |
1 | | elex 3185 |
. 2
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
2 | | eqgval.x |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
3 | | fvex 6113 |
. . . 4
⊢
(Base‘𝐺)
∈ V |
4 | 2, 3 | eqeltri 2684 |
. . 3
⊢ 𝑋 ∈ V |
5 | 4 | ssex 4730 |
. 2
⊢ (𝑆 ⊆ 𝑋 → 𝑆 ∈ V) |
6 | | eqgval.r |
. . 3
⊢ 𝑅 = (𝐺 ~QG 𝑆) |
7 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → 𝑔 = 𝐺) |
8 | 7 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (Base‘𝑔) = (Base‘𝐺)) |
9 | 8, 2 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (Base‘𝑔) = 𝑋) |
10 | 9 | sseq2d 3596 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → ({𝑥, 𝑦} ⊆ (Base‘𝑔) ↔ {𝑥, 𝑦} ⊆ 𝑋)) |
11 | 7 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (+g‘𝑔) = (+g‘𝐺)) |
12 | | eqgval.p |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
13 | 11, 12 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (+g‘𝑔) = + ) |
14 | 7 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (invg‘𝑔) = (invg‘𝐺)) |
15 | | eqgval.n |
. . . . . . . . . 10
⊢ 𝑁 = (invg‘𝐺) |
16 | 14, 15 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (invg‘𝑔) = 𝑁) |
17 | 16 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → ((invg‘𝑔)‘𝑥) = (𝑁‘𝑥)) |
18 | | eqidd 2611 |
. . . . . . . 8
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → 𝑦 = 𝑦) |
19 | 13, 17, 18 | oveq123d 6570 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (((invg‘𝑔)‘𝑥)(+g‘𝑔)𝑦) = ((𝑁‘𝑥) + 𝑦)) |
20 | | simpr 476 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
21 | 19, 20 | eleq12d 2682 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → ((((invg‘𝑔)‘𝑥)(+g‘𝑔)𝑦) ∈ 𝑠 ↔ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)) |
22 | 10, 21 | anbi12d 743 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → (({𝑥, 𝑦} ⊆ (Base‘𝑔) ∧ (((invg‘𝑔)‘𝑥)(+g‘𝑔)𝑦) ∈ 𝑠) ↔ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆))) |
23 | 22 | opabbidv 4648 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑆) → {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑔) ∧ (((invg‘𝑔)‘𝑥)(+g‘𝑔)𝑦) ∈ 𝑠)} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) |
24 | | df-eqg 17416 |
. . . 4
⊢
~QG = (𝑔
∈ V, 𝑠 ∈ V
↦ {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑔) ∧ (((invg‘𝑔)‘𝑥)(+g‘𝑔)𝑦) ∈ 𝑠)}) |
25 | 4, 4 | xpex 6860 |
. . . . 5
⊢ (𝑋 × 𝑋) ∈ V |
26 | | simpl 472 |
. . . . . . . 8
⊢ (({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆) → {𝑥, 𝑦} ⊆ 𝑋) |
27 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
28 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
29 | 27, 28 | prss 4291 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ↔ {𝑥, 𝑦} ⊆ 𝑋) |
30 | 26, 29 | sylibr 223 |
. . . . . . 7
⊢ (({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆) → (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) |
31 | 30 | ssopab2i 4928 |
. . . . . 6
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)} ⊆ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)} |
32 | | df-xp 5044 |
. . . . . 6
⊢ (𝑋 × 𝑋) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)} |
33 | 31, 32 | sseqtr4i 3601 |
. . . . 5
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)} ⊆ (𝑋 × 𝑋) |
34 | 25, 33 | ssexi 4731 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)} ∈ V |
35 | 23, 24, 34 | ovmpt2a 6689 |
. . 3
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → (𝐺 ~QG 𝑆) = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) |
36 | 6, 35 | syl5eq 2656 |
. 2
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V) → 𝑅 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) |
37 | 1, 5, 36 | syl2an 493 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) |