Metamath Proof Explorer

Theorem addscllem1

Description: Lemma for addscl (future) Alternate expression for surreal addition. (Contributed by Scott Fenton, 23-Aug-2024)

Ref Expression
Assertion addscllem1 ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ) |s ( ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 addsval ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑥 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑥 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) } ) ) )
2 addsfn ⊢ +s Fn ( No × No )
3 leftssno ⊢ ( L ‘ 𝐴 ) ⊆ No
4 3 a1i ⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) ⊆ No )
5 snssi ⊢ ( 𝐵 ∈ No → { 𝐵 } ⊆ No )
6 xpss12 ⊢ ( ( ( L ‘ 𝐴 ) ⊆ No ∧ { 𝐵 } ⊆ No ) → ( ( L ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) )
7 4 5 6 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( L ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) )
8 ovelimab ⊢ ( ( +s Fn ( No × No ) ∧ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) ) → ( 𝑥 ∈ ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ∃ 𝑟 ∈ { 𝐵 } 𝑥 = ( 𝑙 +s 𝑟 ) ) )
9 2 7 8 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑥 ∈ ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ∃ 𝑟 ∈ { 𝐵 } 𝑥 = ( 𝑙 +s 𝑟 ) ) )
10 oveq2 ⊢ ( 𝑟 = 𝐵 → ( 𝑙 +s 𝑟 ) = ( 𝑙 +s 𝐵 ) )
11 10 eqeq2d ⊢ ( 𝑟 = 𝐵 → ( 𝑥 = ( 𝑙 +s 𝑟 ) ↔ 𝑥 = ( 𝑙 +s 𝐵 ) ) )
12 11 rexsng ⊢ ( 𝐵 ∈ No → ( ∃ 𝑟 ∈ { 𝐵 } 𝑥 = ( 𝑙 +s 𝑟 ) ↔ 𝑥 = ( 𝑙 +s 𝐵 ) ) )
13 12 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ { 𝐵 } 𝑥 = ( 𝑙 +s 𝑟 ) ↔ 𝑥 = ( 𝑙 +s 𝐵 ) ) )
14 13 rexbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ ( L ‘ 𝐴 ) ∃ 𝑟 ∈ { 𝐵 } 𝑥 = ( 𝑙 +s 𝑟 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) ) )
15 9 14 bitrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑥 ∈ ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) ) )
16 15 abbi2dv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) = { 𝑥 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) } )
17 snssi ⊢ ( 𝐴 ∈ No → { 𝐴 } ⊆ No )
18 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
19 18 a1i ⊢ ( 𝐵 ∈ No → ( L ‘ 𝐵 ) ⊆ No )
20 xpss12 ⊢ ( ( { 𝐴 } ⊆ No ∧ ( L ‘ 𝐵 ) ⊆ No ) → ( { 𝐴 } × ( L ‘ 𝐵 ) ) ⊆ ( No × No ) )
21 17 19 20 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝐴 } × ( L ‘ 𝐵 ) ) ⊆ ( No × No ) )
22 ovelimab ⊢ ( ( +s Fn ( No × No ) ∧ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ⊆ ( No × No ) ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ↔ ∃ 𝑟 ∈ { 𝐴 } ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝑟 +s 𝑙 ) ) )
23 2 21 22 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ↔ ∃ 𝑟 ∈ { 𝐴 } ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝑟 +s 𝑙 ) ) )
24 oveq1 ⊢ ( 𝑟 = 𝐴 → ( 𝑟 +s 𝑙 ) = ( 𝐴 +s 𝑙 ) )
25 24 eqeq2d ⊢ ( 𝑟 = 𝐴 → ( 𝑦 = ( 𝑟 +s 𝑙 ) ↔ 𝑦 = ( 𝐴 +s 𝑙 ) ) )
26 25 rexbidv ⊢ ( 𝑟 = 𝐴 → ( ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝑟 +s 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) ) )
27 26 rexsng ⊢ ( 𝐴 ∈ No → ( ∃ 𝑟 ∈ { 𝐴 } ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝑟 +s 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) ) )
28 27 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ { 𝐴 } ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝑟 +s 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) ) )
29 23 28 bitrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) ) )
30 29 abbi2dv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) } )
31 16 30 uneq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ) = ( { 𝑥 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) } ) )
32 rightssno ⊢ ( R ‘ 𝐴 ) ⊆ No
33 32 a1i ⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) ⊆ No )
34 xpss12 ⊢ ( ( ( R ‘ 𝐴 ) ⊆ No ∧ { 𝐵 } ⊆ No ) → ( ( R ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) )
35 33 5 34 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( R ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) )
36 ovelimab ⊢ ( ( +s Fn ( No × No ) ∧ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ⊆ ( No × No ) ) → ( 𝑥 ∈ ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑙 ∈ { 𝐵 } 𝑥 = ( 𝑟 +s 𝑙 ) ) )
37 2 35 36 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑥 ∈ ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑙 ∈ { 𝐵 } 𝑥 = ( 𝑟 +s 𝑙 ) ) )
38 oveq2 ⊢ ( 𝑙 = 𝐵 → ( 𝑟 +s 𝑙 ) = ( 𝑟 +s 𝐵 ) )
39 38 eqeq2d ⊢ ( 𝑙 = 𝐵 → ( 𝑥 = ( 𝑟 +s 𝑙 ) ↔ 𝑥 = ( 𝑟 +s 𝐵 ) ) )
40 39 rexsng ⊢ ( 𝐵 ∈ No → ( ∃ 𝑙 ∈ { 𝐵 } 𝑥 = ( 𝑟 +s 𝑙 ) ↔ 𝑥 = ( 𝑟 +s 𝐵 ) ) )
41 40 adantl ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ { 𝐵 } 𝑥 = ( 𝑟 +s 𝑙 ) ↔ 𝑥 = ( 𝑟 +s 𝐵 ) ) )
42 41 rexbidv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑟 ∈ ( R ‘ 𝐴 ) ∃ 𝑙 ∈ { 𝐵 } 𝑥 = ( 𝑟 +s 𝑙 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) ) )
43 37 42 bitrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑥 ∈ ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) ) )
44 43 abbi2dv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) = { 𝑥 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) } )
45 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
46 45 a1i ⊢ ( 𝐵 ∈ No → ( R ‘ 𝐵 ) ⊆ No )
47 xpss12 ⊢ ( ( { 𝐴 } ⊆ No ∧ ( R ‘ 𝐵 ) ⊆ No ) → ( { 𝐴 } × ( R ‘ 𝐵 ) ) ⊆ ( No × No ) )
48 17 46 47 syl2an ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( { 𝐴 } × ( R ‘ 𝐵 ) ) ⊆ ( No × No ) )
49 ovelimab ⊢ ( ( +s Fn ( No × No ) ∧ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ⊆ ( No × No ) ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ↔ ∃ 𝑙 ∈ { 𝐴 } ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝑙 +s 𝑟 ) ) )
50 2 48 49 sylancr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ↔ ∃ 𝑙 ∈ { 𝐴 } ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝑙 +s 𝑟 ) ) )
51 oveq1 ⊢ ( 𝑙 = 𝐴 → ( 𝑙 +s 𝑟 ) = ( 𝐴 +s 𝑟 ) )
52 51 eqeq2d ⊢ ( 𝑙 = 𝐴 → ( 𝑦 = ( 𝑙 +s 𝑟 ) ↔ 𝑦 = ( 𝐴 +s 𝑟 ) ) )
53 52 rexbidv ⊢ ( 𝑙 = 𝐴 → ( ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝑙 +s 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) ) )
54 53 rexsng ⊢ ( 𝐴 ∈ No → ( ∃ 𝑙 ∈ { 𝐴 } ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝑙 +s 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) ) )
55 54 adantr ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ∃ 𝑙 ∈ { 𝐴 } ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝑙 +s 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) ) )
56 50 55 bitrd ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝑦 ∈ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) ) )
57 56 abbi2dv ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) = { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) } )
58 44 57 uneq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ) = ( { 𝑥 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) } ) )
59 31 58 oveq12d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( ( ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ) |s ( ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ) ) = ( ( { 𝑥 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑙 ) } ) |s ( { 𝑥 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑥 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑦 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐵 ) 𝑦 = ( 𝐴 +s 𝑟 ) } ) ) )
60 1 59 eqtr4d ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( ( +s “ ( ( L ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( L ‘ 𝐵 ) ) ) ) |s ( ( +s “ ( ( R ‘ 𝐴 ) × { 𝐵 } ) ) ∪ ( +s “ ( { 𝐴 } × ( R ‘ 𝐵 ) ) ) ) ) )