Step | Hyp | Ref
| Expression |
1 | | ecopopr.1 |
. . . . 5
⊢ ∼ =
{〈x, y〉 ∣ ((x ∈ (𝑆 × 𝑆) ∧
y ∈
(𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z + u) = (w + v)))} |
2 | 1 | relopabi 4406 |
. . . 4
⊢ Rel ∼ |
3 | 2 | a1i 9 |
. . 3
⊢ (
⊤ → Rel ∼ ) |
4 | | ecopopr.com |
. . . . 5
⊢ (x + y) = (y + x) |
5 | 1, 4 | ecopovsym 6138 |
. . . 4
⊢ (f ∼ g → g ∼
f) |
6 | 5 | adantl 262 |
. . 3
⊢ ((
⊤ ∧ f ∼ g) → g
∼
f) |
7 | | ecopopr.cl |
. . . . 5
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆) → (x + y) ∈ 𝑆) |
8 | | ecopopr.ass |
. . . . 5
⊢
((x + y) + z) = (x + (y + z)) |
9 | | ecopopr.can |
. . . . 5
⊢
((x ∈ 𝑆 ∧ y ∈ 𝑆) → ((x + y) = (x + z) → y =
z)) |
10 | 1, 4, 7, 8, 9 | ecopovtrn 6139 |
. . . 4
⊢
((f ∼ g ∧ g ∼ ℎ) → f
∼
ℎ) |
11 | 10 | adantl 262 |
. . 3
⊢ ((
⊤ ∧ (f ∼ g ∧ g ∼ ℎ)) → f ∼ ℎ) |
12 | | vex 2554 |
. . . . . . . . . . 11
⊢ g ∈
V |
13 | | vex 2554 |
. . . . . . . . . . 11
⊢ ℎ ∈
V |
14 | 12, 13, 4 | caovcom 5600 |
. . . . . . . . . 10
⊢ (g + ℎ) = (ℎ + g) |
15 | 1 | ecopoveq 6137 |
. . . . . . . . . 10
⊢
(((g ∈ 𝑆 ∧ ℎ ∈
𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈
𝑆)) → (〈g, ℎ〉 ∼ 〈g, ℎ〉 ↔ (g + ℎ) = (ℎ + g))) |
16 | 14, 15 | mpbiri 157 |
. . . . . . . . 9
⊢
(((g ∈ 𝑆 ∧ ℎ ∈
𝑆) ∧ (g ∈ 𝑆 ∧ ℎ ∈
𝑆)) → 〈g, ℎ〉 ∼ 〈g, ℎ〉) |
17 | 16 | anidms 377 |
. . . . . . . 8
⊢
((g ∈ 𝑆 ∧ ℎ ∈
𝑆) → 〈g, ℎ〉 ∼ 〈g, ℎ〉) |
18 | 17 | rgen2a 2369 |
. . . . . . 7
⊢ ∀g ∈ 𝑆 ∀ℎ ∈
𝑆 〈g, ℎ〉 ∼ 〈g, ℎ〉 |
19 | | breq12 3760 |
. . . . . . . . 9
⊢
((f = 〈g, ℎ〉 ∧
f = 〈g, ℎ〉) → (f ∼ f ↔ 〈g, ℎ〉 ∼ 〈g, ℎ〉)) |
20 | 19 | anidms 377 |
. . . . . . . 8
⊢ (f = 〈g,
ℎ〉 → (f ∼ f ↔ 〈g, ℎ〉 ∼ 〈g, ℎ〉)) |
21 | 20 | ralxp 4422 |
. . . . . . 7
⊢ (∀f ∈ (𝑆 × 𝑆)f ∼
f ↔ ∀g ∈ 𝑆 ∀ℎ ∈
𝑆 〈g, ℎ〉 ∼ 〈g, ℎ〉) |
22 | 18, 21 | mpbir 134 |
. . . . . 6
⊢ ∀f ∈ (𝑆 × 𝑆)f ∼
f |
23 | 22 | rspec 2367 |
. . . . 5
⊢ (f ∈ (𝑆 × 𝑆) → f ∼ f) |
24 | 23 | a1i 9 |
. . . 4
⊢ (
⊤ → (f ∈ (𝑆 × 𝑆) → f ∼ f)) |
25 | | opabssxp 4357 |
. . . . . . 7
⊢
{〈x, y〉 ∣ ((x ∈ (𝑆 × 𝑆) ∧
y ∈
(𝑆 × 𝑆)) ∧ ∃z∃w∃v∃u((x =
〈z, w〉 ∧ y = 〈v,
u〉) ∧
(z + u) = (w + v)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
26 | 1, 25 | eqsstri 2969 |
. . . . . 6
⊢ ∼
⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆)) |
27 | 26 | ssbri 3797 |
. . . . 5
⊢ (f ∼ f → f((𝑆 × 𝑆) × (𝑆 × 𝑆))f) |
28 | | brxp 4318 |
. . . . . 6
⊢ (f((𝑆 × 𝑆) × (𝑆 × 𝑆))f
↔ (f ∈ (𝑆 × 𝑆) ∧
f ∈
(𝑆 × 𝑆))) |
29 | 28 | simplbi 259 |
. . . . 5
⊢ (f((𝑆 × 𝑆) × (𝑆 × 𝑆))f
→ f ∈ (𝑆 × 𝑆)) |
30 | 27, 29 | syl 14 |
. . . 4
⊢ (f ∼ f → f ∈ (𝑆 × 𝑆)) |
31 | 24, 30 | impbid1 130 |
. . 3
⊢ (
⊤ → (f ∈ (𝑆 × 𝑆) ↔ f ∼ f)) |
32 | 3, 6, 11, 31 | iserd 6068 |
. 2
⊢ (
⊤ → ∼ Er (𝑆 × 𝑆)) |
33 | 32 | trud 1251 |
1
⊢ ∼ Er
(𝑆 × 𝑆) |