Step | Hyp | Ref
| Expression |
1 | | eqgval.x |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
2 | | eqgval.n |
. . . 4
⊢ 𝑁 = (invg‘𝐺) |
3 | | eqgval.p |
. . . 4
⊢ + =
(+g‘𝐺) |
4 | | eqgval.r |
. . . 4
⊢ 𝑅 = (𝐺 ~QG 𝑆) |
5 | 1, 2, 3, 4 | eqgfval 17642 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}) |
6 | 5 | breqd 4664 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ 𝐴{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}𝐵)) |
7 | | brabv 6699 |
. . . 4
⊢ (𝐴{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
8 | 7 | adantl 482 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ 𝐴{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
9 | | simpr1 1067 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) → 𝐴 ∈ 𝑋) |
10 | | elex 3212 |
. . . . 5
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ V) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) → 𝐴 ∈ V) |
12 | | simpr2 1068 |
. . . . 5
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) → 𝐵 ∈ 𝑋) |
13 | | elex 3212 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ V) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) → 𝐵 ∈ V) |
15 | 11, 14 | jca 554 |
. . 3
⊢ (((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
16 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
17 | | vex 3203 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
18 | 16, 17 | prss 4351 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ↔ {𝑥, 𝑦} ⊆ 𝑋) |
19 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝑋 ↔ 𝐴 ∈ 𝑋)) |
20 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝑦 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) |
21 | 19, 20 | bi2anan9 917 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) |
22 | 18, 21 | syl5bbr 274 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ({𝑥, 𝑦} ⊆ 𝑋 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))) |
23 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑁‘𝑥) = (𝑁‘𝐴)) |
24 | | id 22 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → 𝑦 = 𝐵) |
25 | 23, 24 | oveqan12d 6669 |
. . . . . . 7
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → ((𝑁‘𝑥) + 𝑦) = ((𝑁‘𝐴) + 𝐵)) |
26 | 25 | eleq1d 2686 |
. . . . . 6
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (((𝑁‘𝑥) + 𝑦) ∈ 𝑆 ↔ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) |
27 | 22, 26 | anbi12d 747 |
. . . . 5
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) |
28 | | df-3an 1039 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)) |
29 | 27, 28 | syl6bbr 278 |
. . . 4
⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) |
30 | | eqid 2622 |
. . . 4
⊢
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)} = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)} |
31 | 29, 30 | brabga 4989 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) |
32 | 8, 15, 31 | pm5.21nd 941 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)}𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) |
33 | 6, 32 | bitrd 268 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆))) |