Step | Hyp | Ref
| Expression |
1 | | addsasslem.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | addsasslem.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | 1, 2 | addscut 27292 |
. . . . 5
⊢ (𝜑 → ((𝐴 +s 𝐵) ∈ No
∧ ({𝑑 ∣
∃𝑙 ∈ ( L
‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}))) |
4 | 3 | simp2d 1144 |
. . . 4
⊢ (𝜑 → ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)}) |
5 | 3 | simp3d 1145 |
. . . 4
⊢ (𝜑 → {(𝐴 +s 𝐵)} <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})) |
6 | | ovex 7391 |
. . . . . 6
⊢ (𝐴 +s 𝐵) ∈ V |
7 | 6 | snnz 4738 |
. . . . 5
⊢ {(𝐴 +s 𝐵)} ≠ ∅ |
8 | | sslttr 27149 |
. . . . 5
⊢ ((({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}) ∧ {(𝐴 +s 𝐵)} ≠ ∅) → ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})) |
9 | 7, 8 | mp3an3 1451 |
. . . 4
⊢ ((({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s {(𝐴 +s 𝐵)} ∧ {(𝐴 +s 𝐵)} <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})) → ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})) |
10 | 4, 5, 9 | syl2anc 585 |
. . 3
⊢ (𝜑 → ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) <<s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})) |
11 | | addsasslem.3 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ No
) |
12 | | lltropt 27205 |
. . . 4
⊢ (𝐶 ∈
No → ( L ‘𝐶) <<s ( R ‘𝐶)) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (𝜑 → ( L ‘𝐶) <<s ( R ‘𝐶)) |
14 | | addsval2 27278 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = (({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) |s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}))) |
15 | 1, 2, 14 | syl2anc 585 |
. . 3
⊢ (𝜑 → (𝐴 +s 𝐵) = (({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}) |s ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}))) |
16 | | lrcut 27235 |
. . . . 5
⊢ (𝐶 ∈
No → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
17 | 11, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (( L ‘𝐶) |s ( R ‘𝐶)) = 𝐶) |
18 | 17 | eqcomd 2743 |
. . 3
⊢ (𝜑 → 𝐶 = (( L ‘𝐶) |s ( R ‘𝐶))) |
19 | 10, 13, 15, 18 | addsunif 27313 |
. 2
⊢ (𝜑 → ((𝐴 +s 𝐵) +s 𝐶) = (({𝑦 ∣ ∃ℎ ∈ ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶)} ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |s ({𝑎 ∣ ∃𝑖 ∈ ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶)} ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)}))) |
20 | | unab 4259 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑦 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)}) = {𝑦 ∣ (∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶) ∨ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶))} |
21 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝑧 = ((𝐴 +s 𝑚) +s 𝐶) ↔ 𝑦 = ((𝐴 +s 𝑚) +s 𝐶))) |
22 | 21 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → (∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶) ↔ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶))) |
23 | 22 | cbvabv 2810 |
. . . . . 6
⊢ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)} = {𝑦 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)} |
24 | 23 | uneq2i 4121 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) = ({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑦 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)}) |
25 | | rexun 4151 |
. . . . . . 7
⊢
(∃ℎ ∈
({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶) ↔ (∃ℎ ∈ {𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)}𝑦 = (ℎ +s 𝐶) ∨ ∃ℎ ∈ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}𝑦 = (ℎ +s 𝐶))) |
26 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑑 = ℎ → (𝑑 = (𝑙 +s 𝐵) ↔ ℎ = (𝑙 +s 𝐵))) |
27 | 26 | rexbidv 3176 |
. . . . . . . . . 10
⊢ (𝑑 = ℎ → (∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵) ↔ ∃𝑙 ∈ ( L ‘𝐴)ℎ = (𝑙 +s 𝐵))) |
28 | 27 | rexab 3653 |
. . . . . . . . 9
⊢
(∃ℎ ∈
{𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)}𝑦 = (ℎ +s 𝐶) ↔ ∃ℎ(∃𝑙 ∈ ( L ‘𝐴)ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶))) |
29 | | rexcom4 3272 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈ ( L
‘𝐴)∃ℎ(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃ℎ∃𝑙 ∈ ( L ‘𝐴)(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶))) |
30 | | ovex 7391 |
. . . . . . . . . . . 12
⊢ (𝑙 +s 𝐵) ∈ V |
31 | | oveq1 7365 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝑙 +s 𝐵) → (ℎ +s 𝐶) = ((𝑙 +s 𝐵) +s 𝐶)) |
32 | 31 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑙 +s 𝐵) → (𝑦 = (ℎ +s 𝐶) ↔ 𝑦 = ((𝑙 +s 𝐵) +s 𝐶))) |
33 | 30, 32 | ceqsexv 3495 |
. . . . . . . . . . 11
⊢
(∃ℎ(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ 𝑦 = ((𝑙 +s 𝐵) +s 𝐶)) |
34 | 33 | rexbii 3098 |
. . . . . . . . . 10
⊢
(∃𝑙 ∈ ( L
‘𝐴)∃ℎ(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)) |
35 | | r19.41v 3186 |
. . . . . . . . . . 11
⊢
(∃𝑙 ∈ ( L
‘𝐴)(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ (∃𝑙 ∈ ( L ‘𝐴)ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶))) |
36 | 35 | exbii 1851 |
. . . . . . . . . 10
⊢
(∃ℎ∃𝑙 ∈ ( L ‘𝐴)(ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃ℎ(∃𝑙 ∈ ( L ‘𝐴)ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶))) |
37 | 29, 34, 36 | 3bitr3ri 302 |
. . . . . . . . 9
⊢
(∃ℎ(∃𝑙 ∈ ( L ‘𝐴)ℎ = (𝑙 +s 𝐵) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)) |
38 | 28, 37 | bitri 275 |
. . . . . . . 8
⊢
(∃ℎ ∈
{𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)}𝑦 = (ℎ +s 𝐶) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)) |
39 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑒 = ℎ → (𝑒 = (𝐴 +s 𝑚) ↔ ℎ = (𝐴 +s 𝑚))) |
40 | 39 | rexbidv 3176 |
. . . . . . . . . 10
⊢ (𝑒 = ℎ → (∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝐵)ℎ = (𝐴 +s 𝑚))) |
41 | 40 | rexab 3653 |
. . . . . . . . 9
⊢
(∃ℎ ∈
{𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}𝑦 = (ℎ +s 𝐶) ↔ ∃ℎ(∃𝑚 ∈ ( L ‘𝐵)ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶))) |
42 | | rexcom4 3272 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈ ( L
‘𝐵)∃ℎ(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃ℎ∃𝑚 ∈ ( L ‘𝐵)(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶))) |
43 | | ovex 7391 |
. . . . . . . . . . . 12
⊢ (𝐴 +s 𝑚) ∈ V |
44 | | oveq1 7365 |
. . . . . . . . . . . . 13
⊢ (ℎ = (𝐴 +s 𝑚) → (ℎ +s 𝐶) = ((𝐴 +s 𝑚) +s 𝐶)) |
45 | 44 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝐴 +s 𝑚) → (𝑦 = (ℎ +s 𝐶) ↔ 𝑦 = ((𝐴 +s 𝑚) +s 𝐶))) |
46 | 43, 45 | ceqsexv 3495 |
. . . . . . . . . . 11
⊢
(∃ℎ(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ 𝑦 = ((𝐴 +s 𝑚) +s 𝐶)) |
47 | 46 | rexbii 3098 |
. . . . . . . . . 10
⊢
(∃𝑚 ∈ ( L
‘𝐵)∃ℎ(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)) |
48 | | r19.41v 3186 |
. . . . . . . . . . 11
⊢
(∃𝑚 ∈ ( L
‘𝐵)(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ (∃𝑚 ∈ ( L ‘𝐵)ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶))) |
49 | 48 | exbii 1851 |
. . . . . . . . . 10
⊢
(∃ℎ∃𝑚 ∈ ( L ‘𝐵)(ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃ℎ(∃𝑚 ∈ ( L ‘𝐵)ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶))) |
50 | 42, 47, 49 | 3bitr3ri 302 |
. . . . . . . . 9
⊢
(∃ℎ(∃𝑚 ∈ ( L ‘𝐵)ℎ = (𝐴 +s 𝑚) ∧ 𝑦 = (ℎ +s 𝐶)) ↔ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)) |
51 | 41, 50 | bitri 275 |
. . . . . . . 8
⊢
(∃ℎ ∈
{𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}𝑦 = (ℎ +s 𝐶) ↔ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶)) |
52 | 38, 51 | orbi12i 914 |
. . . . . . 7
⊢
((∃ℎ ∈
{𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)}𝑦 = (ℎ +s 𝐶) ∨ ∃ℎ ∈ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)}𝑦 = (ℎ +s 𝐶)) ↔ (∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶) ∨ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶))) |
53 | 25, 52 | bitri 275 |
. . . . . 6
⊢
(∃ℎ ∈
({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶) ↔ (∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶) ∨ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶))) |
54 | 53 | abbii 2807 |
. . . . 5
⊢ {𝑦 ∣ ∃ℎ ∈ ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶)} = {𝑦 ∣ (∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶) ∨ ∃𝑚 ∈ ( L ‘𝐵)𝑦 = ((𝐴 +s 𝑚) +s 𝐶))} |
55 | 20, 24, 54 | 3eqtr4ri 2776 |
. . . 4
⊢ {𝑦 ∣ ∃ℎ ∈ ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶)} = ({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) |
56 | 55 | uneq1i 4120 |
. . 3
⊢ ({𝑦 ∣ ∃ℎ ∈ ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶)} ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |
57 | | unab 4259 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑎 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)}) = {𝑎 ∣ (∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶) ∨ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶))} |
58 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑏 = 𝑎 → (𝑏 = ((𝐴 +s 𝑞) +s 𝐶) ↔ 𝑎 = ((𝐴 +s 𝑞) +s 𝐶))) |
59 | 58 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑏 = 𝑎 → (∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶) ↔ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶))) |
60 | 59 | cbvabv 2810 |
. . . . . 6
⊢ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)} = {𝑎 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)} |
61 | 60 | uneq2i 4121 |
. . . . 5
⊢ ({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) = ({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑎 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)}) |
62 | | rexun 4151 |
. . . . . . 7
⊢
(∃𝑖 ∈
({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶) ↔ (∃𝑖 ∈ {𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)}𝑎 = (𝑖 +s 𝐶) ∨ ∃𝑖 ∈ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}𝑎 = (𝑖 +s 𝐶))) |
63 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑖 → (𝑓 = (𝑝 +s 𝐵) ↔ 𝑖 = (𝑝 +s 𝐵))) |
64 | 63 | rexbidv 3176 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑖 → (∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵) ↔ ∃𝑝 ∈ ( R ‘𝐴)𝑖 = (𝑝 +s 𝐵))) |
65 | 64 | rexab 3653 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
{𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)}𝑎 = (𝑖 +s 𝐶) ↔ ∃𝑖(∃𝑝 ∈ ( R ‘𝐴)𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶))) |
66 | | rexcom4 3272 |
. . . . . . . . . 10
⊢
(∃𝑝 ∈ ( R
‘𝐴)∃𝑖(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑖∃𝑝 ∈ ( R ‘𝐴)(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶))) |
67 | | ovex 7391 |
. . . . . . . . . . . 12
⊢ (𝑝 +s 𝐵) ∈ V |
68 | | oveq1 7365 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑝 +s 𝐵) → (𝑖 +s 𝐶) = ((𝑝 +s 𝐵) +s 𝐶)) |
69 | 68 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑝 +s 𝐵) → (𝑎 = (𝑖 +s 𝐶) ↔ 𝑎 = ((𝑝 +s 𝐵) +s 𝐶))) |
70 | 67, 69 | ceqsexv 3495 |
. . . . . . . . . . 11
⊢
(∃𝑖(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ 𝑎 = ((𝑝 +s 𝐵) +s 𝐶)) |
71 | 70 | rexbii 3098 |
. . . . . . . . . 10
⊢
(∃𝑝 ∈ ( R
‘𝐴)∃𝑖(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)) |
72 | | r19.41v 3186 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈ ( R
‘𝐴)(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ (∃𝑝 ∈ ( R ‘𝐴)𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶))) |
73 | 72 | exbii 1851 |
. . . . . . . . . 10
⊢
(∃𝑖∃𝑝 ∈ ( R ‘𝐴)(𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑖(∃𝑝 ∈ ( R ‘𝐴)𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶))) |
74 | 66, 71, 73 | 3bitr3ri 302 |
. . . . . . . . 9
⊢
(∃𝑖(∃𝑝 ∈ ( R ‘𝐴)𝑖 = (𝑝 +s 𝐵) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)) |
75 | 65, 74 | bitri 275 |
. . . . . . . 8
⊢
(∃𝑖 ∈
{𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)}𝑎 = (𝑖 +s 𝐶) ↔ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)) |
76 | | eqeq1 2741 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑖 → (𝑔 = (𝐴 +s 𝑞) ↔ 𝑖 = (𝐴 +s 𝑞))) |
77 | 76 | rexbidv 3176 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑖 → (∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞) ↔ ∃𝑞 ∈ ( R ‘𝐵)𝑖 = (𝐴 +s 𝑞))) |
78 | 77 | rexab 3653 |
. . . . . . . . 9
⊢
(∃𝑖 ∈
{𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}𝑎 = (𝑖 +s 𝐶) ↔ ∃𝑖(∃𝑞 ∈ ( R ‘𝐵)𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶))) |
79 | | rexcom4 3272 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈ ( R
‘𝐵)∃𝑖(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑖∃𝑞 ∈ ( R ‘𝐵)(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶))) |
80 | | ovex 7391 |
. . . . . . . . . . . 12
⊢ (𝐴 +s 𝑞) ∈ V |
81 | | oveq1 7365 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝐴 +s 𝑞) → (𝑖 +s 𝐶) = ((𝐴 +s 𝑞) +s 𝐶)) |
82 | 81 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝐴 +s 𝑞) → (𝑎 = (𝑖 +s 𝐶) ↔ 𝑎 = ((𝐴 +s 𝑞) +s 𝐶))) |
83 | 80, 82 | ceqsexv 3495 |
. . . . . . . . . . 11
⊢
(∃𝑖(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ 𝑎 = ((𝐴 +s 𝑞) +s 𝐶)) |
84 | 83 | rexbii 3098 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈ ( R
‘𝐵)∃𝑖(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)) |
85 | | r19.41v 3186 |
. . . . . . . . . . 11
⊢
(∃𝑞 ∈ ( R
‘𝐵)(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ (∃𝑞 ∈ ( R ‘𝐵)𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶))) |
86 | 85 | exbii 1851 |
. . . . . . . . . 10
⊢
(∃𝑖∃𝑞 ∈ ( R ‘𝐵)(𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑖(∃𝑞 ∈ ( R ‘𝐵)𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶))) |
87 | 79, 84, 86 | 3bitr3ri 302 |
. . . . . . . . 9
⊢
(∃𝑖(∃𝑞 ∈ ( R ‘𝐵)𝑖 = (𝐴 +s 𝑞) ∧ 𝑎 = (𝑖 +s 𝐶)) ↔ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)) |
88 | 78, 87 | bitri 275 |
. . . . . . . 8
⊢
(∃𝑖 ∈
{𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}𝑎 = (𝑖 +s 𝐶) ↔ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶)) |
89 | 75, 88 | orbi12i 914 |
. . . . . . 7
⊢
((∃𝑖 ∈
{𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)}𝑎 = (𝑖 +s 𝐶) ∨ ∃𝑖 ∈ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)}𝑎 = (𝑖 +s 𝐶)) ↔ (∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶) ∨ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶))) |
90 | 62, 89 | bitri 275 |
. . . . . 6
⊢
(∃𝑖 ∈
({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶) ↔ (∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶) ∨ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶))) |
91 | 90 | abbii 2807 |
. . . . 5
⊢ {𝑎 ∣ ∃𝑖 ∈ ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶)} = {𝑎 ∣ (∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶) ∨ ∃𝑞 ∈ ( R ‘𝐵)𝑎 = ((𝐴 +s 𝑞) +s 𝐶))} |
92 | 57, 61, 91 | 3eqtr4ri 2776 |
. . . 4
⊢ {𝑎 ∣ ∃𝑖 ∈ ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶)} = ({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) |
93 | 92 | uneq1i 4120 |
. . 3
⊢ ({𝑎 ∣ ∃𝑖 ∈ ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶)} ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)}) = (({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)}) |
94 | 56, 93 | oveq12i 7370 |
. 2
⊢ (({𝑦 ∣ ∃ℎ ∈ ({𝑑 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑑 = (𝑙 +s 𝐵)} ∪ {𝑒 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑒 = (𝐴 +s 𝑚)})𝑦 = (ℎ +s 𝐶)} ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |s ({𝑎 ∣ ∃𝑖 ∈ ({𝑓 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑓 = (𝑝 +s 𝐵)} ∪ {𝑔 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑔 = (𝐴 +s 𝑞)})𝑎 = (𝑖 +s 𝐶)} ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)})) = ((({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |s (({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)})) |
95 | 19, 94 | eqtrdi 2793 |
1
⊢ (𝜑 → ((𝐴 +s 𝐵) +s 𝐶) = ((({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = ((𝑙 +s 𝐵) +s 𝐶)} ∪ {𝑧 ∣ ∃𝑚 ∈ ( L ‘𝐵)𝑧 = ((𝐴 +s 𝑚) +s 𝐶)}) ∪ {𝑤 ∣ ∃𝑛 ∈ ( L ‘𝐶)𝑤 = ((𝐴 +s 𝐵) +s 𝑛)}) |s (({𝑎 ∣ ∃𝑝 ∈ ( R ‘𝐴)𝑎 = ((𝑝 +s 𝐵) +s 𝐶)} ∪ {𝑏 ∣ ∃𝑞 ∈ ( R ‘𝐵)𝑏 = ((𝐴 +s 𝑞) +s 𝐶)}) ∪ {𝑐 ∣ ∃𝑟 ∈ ( R ‘𝐶)𝑐 = ((𝐴 +s 𝐵) +s 𝑟)}))) |