Step | Hyp | Ref
| Expression |
1 | | relopab 4752 |
. 2
⊢ Rel
{⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} |
2 | | releqg.r |
. . . 4
⊢ 𝑅 = (𝐺 ~QG 𝑆) |
3 | | elex 2748 |
. . . . . 6
⊢ (𝐺 ∈ 𝑉 → 𝐺 ∈ V) |
4 | 3 | adantr 276 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝐺 ∈ V) |
5 | | elex 2748 |
. . . . . 6
⊢ (𝑆 ∈ 𝑊 → 𝑆 ∈ V) |
6 | 5 | adantl 277 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝑆 ∈ V) |
7 | | vex 2740 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
8 | | vex 2740 |
. . . . . . . . 9
⊢ 𝑦 ∈ V |
9 | 7, 8 | prss 3748 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐺)) |
10 | 9 | anbi1i 458 |
. . . . . . 7
⊢ (((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆) ↔ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)) |
11 | 10 | opabbii 4069 |
. . . . . 6
⊢
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} |
12 | | basfn 12512 |
. . . . . . . . 9
⊢ Base Fn
V |
13 | | funfvex 5531 |
. . . . . . . . . 10
⊢ ((Fun
Base ∧ 𝐺 ∈ dom
Base) → (Base‘𝐺)
∈ V) |
14 | 13 | funfni 5315 |
. . . . . . . . 9
⊢ ((Base Fn
V ∧ 𝐺 ∈ V) →
(Base‘𝐺) ∈
V) |
15 | 12, 4, 14 | sylancr 414 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (Base‘𝐺) ∈ V) |
16 | | xpexg 4739 |
. . . . . . . 8
⊢
(((Base‘𝐺)
∈ V ∧ (Base‘𝐺) ∈ V) → ((Base‘𝐺) × (Base‘𝐺)) ∈ V) |
17 | 15, 15, 16 | syl2anc 411 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → ((Base‘𝐺) × (Base‘𝐺)) ∈ V) |
18 | | opabssxp 4699 |
. . . . . . . 8
⊢
{⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} ⊆ ((Base‘𝐺) × (Base‘𝐺)) |
19 | 18 | a1i 9 |
. . . . . . 7
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} ⊆ ((Base‘𝐺) × (Base‘𝐺))) |
20 | 17, 19 | ssexd 4142 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} ∈ V) |
21 | 11, 20 | eqeltrrid 2265 |
. . . . 5
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} ∈ V) |
22 | | fveq2 5514 |
. . . . . . . . 9
⊢ (𝑟 = 𝐺 → (Base‘𝑟) = (Base‘𝐺)) |
23 | 22 | sseq2d 3185 |
. . . . . . . 8
⊢ (𝑟 = 𝐺 → ({𝑥, 𝑦} ⊆ (Base‘𝑟) ↔ {𝑥, 𝑦} ⊆ (Base‘𝐺))) |
24 | | fveq2 5514 |
. . . . . . . . . 10
⊢ (𝑟 = 𝐺 → (+g‘𝑟) = (+g‘𝐺)) |
25 | | fveq2 5514 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝐺 → (invg‘𝑟) = (invg‘𝐺)) |
26 | 25 | fveq1d 5516 |
. . . . . . . . . 10
⊢ (𝑟 = 𝐺 → ((invg‘𝑟)‘𝑥) = ((invg‘𝐺)‘𝑥)) |
27 | | eqidd 2178 |
. . . . . . . . . 10
⊢ (𝑟 = 𝐺 → 𝑦 = 𝑦) |
28 | 24, 26, 27 | oveq123d 5893 |
. . . . . . . . 9
⊢ (𝑟 = 𝐺 → (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) = (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦)) |
29 | 28 | eleq1d 2246 |
. . . . . . . 8
⊢ (𝑟 = 𝐺 → ((((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖 ↔ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖)) |
30 | 23, 29 | anbi12d 473 |
. . . . . . 7
⊢ (𝑟 = 𝐺 → (({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖) ↔ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖))) |
31 | 30 | opabbidv 4068 |
. . . . . 6
⊢ (𝑟 = 𝐺 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖)}) |
32 | | eleq2 2241 |
. . . . . . . 8
⊢ (𝑖 = 𝑆 → ((((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖 ↔ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)) |
33 | 32 | anbi2d 464 |
. . . . . . 7
⊢ (𝑖 = 𝑆 → (({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖) ↔ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆))) |
34 | 33 | opabbidv 4068 |
. . . . . 6
⊢ (𝑖 = 𝑆 → {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑖)} = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)}) |
35 | | df-eqg 12963 |
. . . . . 6
⊢
~QG = (𝑟
∈ V, 𝑖 ∈ V
↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)}) |
36 | 31, 34, 35 | ovmpog 6006 |
. . . . 5
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ V ∧ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)} ∈ V) → (𝐺 ~QG 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)}) |
37 | 4, 6, 21, 36 | syl3anc 1238 |
. . . 4
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐺 ~QG 𝑆) = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)}) |
38 | 2, 37 | eqtrid 2222 |
. . 3
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)}) |
39 | 38 | releqd 4709 |
. 2
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (Rel 𝑅 ↔ Rel {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝐺) ∧ (((invg‘𝐺)‘𝑥)(+g‘𝐺)𝑦) ∈ 𝑆)})) |
40 | 1, 39 | mpbiri 168 |
1
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → Rel 𝑅) |