Step | Hyp | Ref
| Expression |
1 | | simpl 108 |
. . . . . . . 8
⊢ (((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) → (𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆)) |
2 | 1 | reximi 2561 |
. . . . . . 7
⊢
(∃𝑞 ∈
𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) → ∃𝑞 ∈ 𝐵 (𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆)) |
3 | 2 | reximi 2561 |
. . . . . 6
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 (𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆)) |
4 | | eropr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (𝐴 / 𝑅) |
5 | 4 | eleq2i 2231 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐽 ↔ 𝑥 ∈ (𝐴 / 𝑅)) |
6 | | vex 2727 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
7 | 6 | elqs 6546 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐴 / 𝑅) ↔ ∃𝑝 ∈ 𝐴 𝑥 = [𝑝]𝑅) |
8 | 5, 7 | bitri 183 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐽 ↔ ∃𝑝 ∈ 𝐴 𝑥 = [𝑝]𝑅) |
9 | | eropr.2 |
. . . . . . . . . 10
⊢ 𝐾 = (𝐵 / 𝑆) |
10 | 9 | eleq2i 2231 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐾 ↔ 𝑦 ∈ (𝐵 / 𝑆)) |
11 | | vex 2727 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
12 | 11 | elqs 6546 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐵 / 𝑆) ↔ ∃𝑞 ∈ 𝐵 𝑦 = [𝑞]𝑆) |
13 | 10, 12 | bitri 183 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐾 ↔ ∃𝑞 ∈ 𝐵 𝑦 = [𝑞]𝑆) |
14 | 8, 13 | anbi12i 456 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ↔ (∃𝑝 ∈ 𝐴 𝑥 = [𝑝]𝑅 ∧ ∃𝑞 ∈ 𝐵 𝑦 = [𝑞]𝑆)) |
15 | | reeanv 2633 |
. . . . . . 7
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 (𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ↔ (∃𝑝 ∈ 𝐴 𝑥 = [𝑝]𝑅 ∧ ∃𝑞 ∈ 𝐵 𝑦 = [𝑞]𝑆)) |
16 | 14, 15 | bitr4i 186 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 (𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆)) |
17 | 3, 16 | sylibr 133 |
. . . . 5
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) → (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) |
18 | 17 | pm4.71ri 390 |
. . . 4
⊢
(∃𝑝 ∈
𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
19 | | eropr.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ∈ 𝑍) |
20 | | eropr.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Er 𝑈) |
21 | | eropr.5 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 Er 𝑉) |
22 | | eropr.6 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 Er 𝑊) |
23 | | eropr.7 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝑈) |
24 | | eropr.8 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ 𝑉) |
25 | | eropr.9 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ⊆ 𝑊) |
26 | | eropr.10 |
. . . . . . . 8
⊢ (𝜑 → + :(𝐴 × 𝐵)⟶𝐶) |
27 | | eropr.11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑟𝑅𝑠 ∧ 𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢))) |
28 | 4, 9, 19, 20, 21, 22, 23, 24, 25, 26, 27 | eroveu 6586 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
29 | | iota1 5164 |
. . . . . . 7
⊢
(∃!𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) = 𝑧)) |
30 | 28, 29 | syl 14 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) = 𝑧)) |
31 | | eqcom 2166 |
. . . . . 6
⊢
((℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) = 𝑧 ↔ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
32 | 30, 31 | bitrdi 195 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
33 | 32 | pm5.32da 448 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))) |
34 | 18, 33 | syl5bb 191 |
. . 3
⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))) |
35 | 34 | oprabbidv 5890 |
. 2
⊢ (𝜑 → {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))}) |
36 | | eropr.12 |
. 2
⊢ ⨣ =
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)} |
37 | | df-mpo 5844 |
. . 3
⊢ (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))} |
38 | | nfv 1515 |
. . . 4
⊢
Ⅎ𝑤((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
39 | | nfv 1515 |
. . . . 5
⊢
Ⅎ𝑧(𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) |
40 | | nfiota1 5152 |
. . . . . 6
⊢
Ⅎ𝑧(℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
41 | 40 | nfeq2 2318 |
. . . . 5
⊢
Ⅎ𝑧 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) |
42 | 39, 41 | nfan 1552 |
. . . 4
⊢
Ⅎ𝑧((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) |
43 | | eqeq1 2171 |
. . . . 5
⊢ (𝑧 = 𝑤 → (𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)) ↔ 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |
44 | 43 | anbi2d 460 |
. . . 4
⊢ (𝑧 = 𝑤 → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) ↔ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))))) |
45 | 38, 42, 44 | cbvoprab3 5912 |
. . 3
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))} = {〈〈𝑥, 𝑦〉, 𝑤〉 ∣ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑤 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))} |
46 | 37, 45 | eqtr4i 2188 |
. 2
⊢ (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ ((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾) ∧ 𝑧 = (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))} |
47 | 35, 36, 46 | 3eqtr4g 2222 |
1
⊢ (𝜑 → ⨣ = (𝑥 ∈ 𝐽, 𝑦 ∈ 𝐾 ↦ (℩𝑧∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ((𝑥 = [𝑝]𝑅 ∧ 𝑦 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇)))) |