Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . . . . 8
⊢
(((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → (x = [𝑝]𝑅 ∧ y = [𝑞]𝑆)) |
2 | 1 | reximi 2410 |
. . . . . . 7
⊢ (∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → ∃𝑞 ∈ B (x = [𝑝]𝑅 ∧ y = [𝑞]𝑆)) |
3 | 2 | reximi 2410 |
. . . . . 6
⊢ (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → ∃𝑝 ∈ A ∃𝑞 ∈ B (x = [𝑝]𝑅 ∧ y = [𝑞]𝑆)) |
4 | | eropr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (A / 𝑅) |
5 | 4 | eleq2i 2101 |
. . . . . . . . 9
⊢ (x ∈ 𝐽 ↔ x ∈ (A / 𝑅)) |
6 | | vex 2554 |
. . . . . . . . . 10
⊢ x ∈
V |
7 | 6 | elqs 6093 |
. . . . . . . . 9
⊢ (x ∈ (A / 𝑅) ↔ ∃𝑝 ∈ A x = [𝑝]𝑅) |
8 | 5, 7 | bitri 173 |
. . . . . . . 8
⊢ (x ∈ 𝐽 ↔ ∃𝑝 ∈ A x = [𝑝]𝑅) |
9 | | eropr.2 |
. . . . . . . . . 10
⊢ 𝐾 = (B / 𝑆) |
10 | 9 | eleq2i 2101 |
. . . . . . . . 9
⊢ (y ∈ 𝐾 ↔ y ∈ (B / 𝑆)) |
11 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
12 | 11 | elqs 6093 |
. . . . . . . . 9
⊢ (y ∈ (B / 𝑆) ↔ ∃𝑞 ∈ B y = [𝑞]𝑆) |
13 | 10, 12 | bitri 173 |
. . . . . . . 8
⊢ (y ∈ 𝐾 ↔ ∃𝑞 ∈ B y = [𝑞]𝑆) |
14 | 8, 13 | anbi12i 433 |
. . . . . . 7
⊢
((x ∈ 𝐽 ∧ y ∈ 𝐾) ↔ (∃𝑝 ∈ A x = [𝑝]𝑅 ∧ ∃𝑞 ∈ B y = [𝑞]𝑆)) |
15 | | reeanv 2473 |
. . . . . . 7
⊢ (∃𝑝 ∈ A ∃𝑞 ∈ B (x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ↔ (∃𝑝 ∈ A x = [𝑝]𝑅 ∧ ∃𝑞 ∈ B y = [𝑞]𝑆)) |
16 | 14, 15 | bitr4i 176 |
. . . . . 6
⊢
((x ∈ 𝐽 ∧ y ∈ 𝐾) ↔ ∃𝑝 ∈ A ∃𝑞 ∈ B (x = [𝑝]𝑅 ∧ y = [𝑞]𝑆)) |
17 | 3, 16 | sylibr 137 |
. . . . 5
⊢ (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → (x ∈ 𝐽 ∧ y ∈ 𝐾)) |
18 | 17 | pm4.71ri 372 |
. . . 4
⊢ (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) ↔ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) |
19 | | eropr.3 |
. . . . . . . 8
⊢ (φ → 𝑇 ∈ 𝑍) |
20 | | eropr.4 |
. . . . . . . 8
⊢ (φ → 𝑅 Er 𝑈) |
21 | | eropr.5 |
. . . . . . . 8
⊢ (φ → 𝑆 Er 𝑉) |
22 | | eropr.6 |
. . . . . . . 8
⊢ (φ → 𝑇 Er 𝑊) |
23 | | eropr.7 |
. . . . . . . 8
⊢ (φ → A ⊆ 𝑈) |
24 | | eropr.8 |
. . . . . . . 8
⊢ (φ → B ⊆ 𝑉) |
25 | | eropr.9 |
. . . . . . . 8
⊢ (φ → 𝐶 ⊆ 𝑊) |
26 | | eropr.10 |
. . . . . . . 8
⊢ (φ → + :(A × B)⟶𝐶) |
27 | | eropr.11 |
. . . . . . . 8
⊢ ((φ ∧ ((𝑟 ∈ A ∧ 𝑠
∈ A)
∧ (𝑡 ∈ B ∧ u ∈ B))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆u)
→ (𝑟 + 𝑡)𝑇(𝑠 + u))) |
28 | 4, 9, 19, 20, 21, 22, 23, 24, 25, 26, 27 | eroveu 6133 |
. . . . . . 7
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → ∃!z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) |
29 | | iota1 4824 |
. . . . . . 7
⊢ (∃!z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) → (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) ↔ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) = z)) |
30 | 28, 29 | syl 14 |
. . . . . 6
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) ↔ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) = z)) |
31 | | eqcom 2039 |
. . . . . 6
⊢
((℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) = z
↔ z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) |
32 | 30, 31 | syl6bb 185 |
. . . . 5
⊢ ((φ ∧
(x ∈
𝐽 ∧ y ∈ 𝐾)) → (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) ↔ z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))) |
33 | 32 | pm5.32da 425 |
. . . 4
⊢ (φ → (((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ↔ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))))) |
34 | 18, 33 | syl5bb 181 |
. . 3
⊢ (φ → (∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇) ↔ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))))) |
35 | 34 | oprabbidv 5501 |
. 2
⊢ (φ → {〈〈x, y〉,
z〉 ∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)} = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))}) |
36 | | eropr.12 |
. 2
⊢ ⨣ =
{〈〈x, y〉, z〉
∣ ∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)} |
37 | | df-mpt2 5460 |
. . 3
⊢ (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) = {〈〈x, y〉,
w〉 ∣ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))} |
38 | | nfv 1418 |
. . . 4
⊢
Ⅎw((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) |
39 | | nfv 1418 |
. . . . 5
⊢
Ⅎz(x ∈ 𝐽 ∧ y ∈ 𝐾) |
40 | | nfiota1 4812 |
. . . . . 6
⊢
Ⅎz(℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) |
41 | 40 | nfeq2 2186 |
. . . . 5
⊢
Ⅎz w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) |
42 | 39, 41 | nfan 1454 |
. . . 4
⊢
Ⅎz((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) |
43 | | eqeq1 2043 |
. . . . 5
⊢ (z = w →
(z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)) ↔ w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))) |
44 | 43 | anbi2d 437 |
. . . 4
⊢ (z = w →
(((x ∈
𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) ↔ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))))) |
45 | 38, 42, 44 | cbvoprab3 5522 |
. . 3
⊢
{〈〈x, y〉, z〉
∣ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧ z =
(℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))} = {〈〈x, y〉,
w〉 ∣ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
w = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))} |
46 | 37, 45 | eqtr4i 2060 |
. 2
⊢ (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇))) = {〈〈x, y〉,
z〉 ∣ ((x ∈ 𝐽 ∧ y ∈ 𝐾) ∧
z = (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))} |
47 | 35, 36, 46 | 3eqtr4g 2094 |
1
⊢ (φ → ⨣ = (x ∈ 𝐽, y ∈ 𝐾 ↦ (℩z∃𝑝 ∈ A ∃𝑞 ∈ B ((x = [𝑝]𝑅 ∧ y = [𝑞]𝑆) ∧
z = [(𝑝 + 𝑞)]𝑇)))) |