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