Step | Hyp | Ref
| Expression |
1 | | addsov 33710 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = (({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}) |s ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)}))) |
2 | | addsfn 33709 |
. . . . . . 7
⊢ +s Fn
( No × No
) |
3 | | leftssno 33655 |
. . . . . . . 8
⊢ (𝐴 ∈
No → ( L ‘𝐴) ⊆ No
) |
4 | | snssi 4701 |
. . . . . . . 8
⊢ (𝐵 ∈
No → {𝐵}
⊆ No ) |
5 | | xpss12 5543 |
. . . . . . . 8
⊢ ((( L
‘𝐴) ⊆ No ∧ {𝐵} ⊆ No )
→ (( L ‘𝐴)
× {𝐵}) ⊆ ( No × No
)) |
6 | 3, 4, 5 | syl2an 598 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( L ‘𝐴) × {𝐵}) ⊆ ( No
× No )) |
7 | | ovelimab 7328 |
. . . . . . 7
⊢ (( +s Fn
( No × No )
∧ (( L ‘𝐴)
× {𝐵}) ⊆ ( No × No )) →
(𝑥 ∈ ( +s “ (( L
‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟))) |
8 | 2, 6, 7 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑥 ∈ ( +s “ (( L ‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟))) |
9 | | oveq2 7164 |
. . . . . . . . . 10
⊢ (𝑟 = 𝐵 → (𝑙 +s 𝑟) = (𝑙 +s 𝐵)) |
10 | 9 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑟 = 𝐵 → (𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵))) |
11 | 10 | rexsng 4574 |
. . . . . . . 8
⊢ (𝐵 ∈
No → (∃𝑟
∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵))) |
12 | 11 | adantl 485 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ 𝑥 = (𝑙 +s 𝐵))) |
13 | 12 | rexbidv 3221 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑙 ∈ ( L ‘𝐴)∃𝑟 ∈ {𝐵}𝑥 = (𝑙 +s 𝑟) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵))) |
14 | 8, 13 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑥 ∈ ( +s “ (( L ‘𝐴) × {𝐵})) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵))) |
15 | 14 | abbi2dv 2889 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( +s “ (( L ‘𝐴) × {𝐵})) = {𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)}) |
16 | | snssi 4701 |
. . . . . . . 8
⊢ (𝐴 ∈
No → {𝐴}
⊆ No ) |
17 | | leftssno 33655 |
. . . . . . . 8
⊢ (𝐵 ∈
No → ( L ‘𝐵) ⊆ No
) |
18 | | xpss12 5543 |
. . . . . . . 8
⊢ (({𝐴} ⊆
No ∧ ( L ‘𝐵) ⊆ No )
→ ({𝐴} × ( L
‘𝐵)) ⊆ ( No × No
)) |
19 | 16, 17, 18 | syl2an 598 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝐴} × ( L ‘𝐵)) ⊆ ( No
× No )) |
20 | | ovelimab 7328 |
. . . . . . 7
⊢ (( +s Fn
( No × No )
∧ ({𝐴} × ( L
‘𝐵)) ⊆ ( No × No )) →
(𝑦 ∈ ( +s “
({𝐴} × ( L
‘𝐵))) ↔
∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙))) |
21 | 2, 19, 20 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( L ‘𝐵))) ↔ ∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙))) |
22 | | oveq1 7163 |
. . . . . . . . . 10
⊢ (𝑟 = 𝐴 → (𝑟 +s 𝑙) = (𝐴 +s 𝑙)) |
23 | 22 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑟 = 𝐴 → (𝑦 = (𝑟 +s 𝑙) ↔ 𝑦 = (𝐴 +s 𝑙))) |
24 | 23 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑟 = 𝐴 → (∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙))) |
25 | 24 | rexsng 4574 |
. . . . . . 7
⊢ (𝐴 ∈
No → (∃𝑟
∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙))) |
26 | 25 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑟 ∈ {𝐴}∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝑟 +s 𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙))) |
27 | 21, 26 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( L ‘𝐵))) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙))) |
28 | 27 | abbi2dv 2889 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( +s “ ({𝐴} × ( L ‘𝐵))) = {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}) |
29 | 15, 28 | uneq12d 4071 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) = ({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)})) |
30 | | rightssno 33656 |
. . . . . . . 8
⊢ (𝐴 ∈
No → ( R ‘𝐴) ⊆ No
) |
31 | | xpss12 5543 |
. . . . . . . 8
⊢ ((( R
‘𝐴) ⊆ No ∧ {𝐵} ⊆ No )
→ (( R ‘𝐴)
× {𝐵}) ⊆ ( No × No
)) |
32 | 30, 4, 31 | syl2an 598 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( R ‘𝐴) × {𝐵}) ⊆ ( No
× No )) |
33 | | ovelimab 7328 |
. . . . . . 7
⊢ (( +s Fn
( No × No )
∧ (( R ‘𝐴)
× {𝐵}) ⊆ ( No × No )) →
(𝑥 ∈ ( +s “ (( R
‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙))) |
34 | 2, 32, 33 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑥 ∈ ( +s “ (( R ‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙))) |
35 | | oveq2 7164 |
. . . . . . . . . 10
⊢ (𝑙 = 𝐵 → (𝑟 +s 𝑙) = (𝑟 +s 𝐵)) |
36 | 35 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑙 = 𝐵 → (𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵))) |
37 | 36 | rexsng 4574 |
. . . . . . . 8
⊢ (𝐵 ∈
No → (∃𝑙
∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵))) |
38 | 37 | adantl 485 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ 𝑥 = (𝑟 +s 𝐵))) |
39 | 38 | rexbidv 3221 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑟 ∈ ( R ‘𝐴)∃𝑙 ∈ {𝐵}𝑥 = (𝑟 +s 𝑙) ↔ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵))) |
40 | 34, 39 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑥 ∈ ( +s “ (( R ‘𝐴) × {𝐵})) ↔ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵))) |
41 | 40 | abbi2dv 2889 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( +s “ (( R ‘𝐴) × {𝐵})) = {𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)}) |
42 | | rightssno 33656 |
. . . . . . . 8
⊢ (𝐵 ∈
No → ( R ‘𝐵) ⊆ No
) |
43 | | xpss12 5543 |
. . . . . . . 8
⊢ (({𝐴} ⊆
No ∧ ( R ‘𝐵) ⊆ No )
→ ({𝐴} × ( R
‘𝐵)) ⊆ ( No × No
)) |
44 | 16, 42, 43 | syl2an 598 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝐴} × ( R ‘𝐵)) ⊆ ( No
× No )) |
45 | | ovelimab 7328 |
. . . . . . 7
⊢ (( +s Fn
( No × No )
∧ ({𝐴} × ( R
‘𝐵)) ⊆ ( No × No )) →
(𝑦 ∈ ( +s “
({𝐴} × ( R
‘𝐵))) ↔
∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟))) |
46 | 2, 44, 45 | sylancr 590 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( R ‘𝐵))) ↔ ∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟))) |
47 | | oveq1 7163 |
. . . . . . . . . 10
⊢ (𝑙 = 𝐴 → (𝑙 +s 𝑟) = (𝐴 +s 𝑟)) |
48 | 47 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑙 = 𝐴 → (𝑦 = (𝑙 +s 𝑟) ↔ 𝑦 = (𝐴 +s 𝑟))) |
49 | 48 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑙 = 𝐴 → (∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟))) |
50 | 49 | rexsng 4574 |
. . . . . . 7
⊢ (𝐴 ∈
No → (∃𝑙
∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟))) |
51 | 50 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑙 ∈ {𝐴}∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝑙 +s 𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟))) |
52 | 46, 51 | bitrd 282 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑦 ∈ ( +s “ ({𝐴} × ( R ‘𝐵))) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟))) |
53 | 52 | abbi2dv 2889 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( +s “ ({𝐴} × ( R ‘𝐵))) = {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)}) |
54 | 41, 53 | uneq12d 4071 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵)))) = ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)})) |
55 | 29, 54 | oveq12d 7174 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) |s (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵))))) = (({𝑥 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑥 = (𝑙 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑦 = (𝐴 +s 𝑙)}) |s ({𝑥 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑥 = (𝑟 +s 𝐵)} ∪ {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑦 = (𝐴 +s 𝑟)}))) |
56 | 1, 55 | eqtr4d 2796 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = ((( +s “ (( L ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( L ‘𝐵)))) |s (( +s “ (( R ‘𝐴) × {𝐵})) ∪ ( +s “ ({𝐴} × ( R ‘𝐵)))))) |