Metamath Proof Explorer

Theorem addsid1

Description: Surreal addition to zero is identity. Part of Theorem 3 of Conway p. 17. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion addsid1 ( 𝐴 ∈ No → ( 𝐴 +s 0s ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 +s 0s ) = ( 𝑏 +s 0s ) )
2 id ⊢ ( 𝑎 = 𝑏 → 𝑎 = 𝑏 )
3 1 2 eqeq12d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 +s 0s ) = 𝑎 ↔ ( 𝑏 +s 0s ) = 𝑏 ) )
4 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 +s 0s ) = ( 𝐴 +s 0s ) )
5 id ⊢ ( 𝑎 = 𝐴 → 𝑎 = 𝐴 )
6 4 5 eqeq12d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 +s 0s ) = 𝑎 ↔ ( 𝐴 +s 0s ) = 𝐴 ) )
7 0sno ⊢ 0s ∈ No
8 addsov ⊢ ( ( 𝑎 ∈ No ∧ 0s ∈ No ) → ( 𝑎 +s 0s ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) ) )
9 7 8 mpan2 ⊢ ( 𝑎 ∈ No → ( 𝑎 +s 0s ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) ) )
10 9 adantr ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( 𝑎 +s 0s ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) ) )
11 elun1 ⊢ ( 𝑦 ∈ ( L ‘ 𝑎 ) → 𝑦 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) )
12 simpr ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 )
13 oveq1 ⊢ ( 𝑏 = 𝑦 → ( 𝑏 +s 0s ) = ( 𝑦 +s 0s ) )
14 id ⊢ ( 𝑏 = 𝑦 → 𝑏 = 𝑦 )
15 13 14 eqeq12d ⊢ ( 𝑏 = 𝑦 → ( ( 𝑏 +s 0s ) = 𝑏 ↔ ( 𝑦 +s 0s ) = 𝑦 ) )
16 15 rspcva ⊢ ( ( 𝑦 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( 𝑦 +s 0s ) = 𝑦 )
17 11 12 16 syl2anr ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑦 ∈ ( L ‘ 𝑎 ) ) → ( 𝑦 +s 0s ) = 𝑦 )
18 17 eqeq2d ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑦 ∈ ( L ‘ 𝑎 ) ) → ( 𝑥 = ( 𝑦 +s 0s ) ↔ 𝑥 = 𝑦 ) )
19 equcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
20 18 19 bitrdi ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑦 ∈ ( L ‘ 𝑎 ) ) → ( 𝑥 = ( 𝑦 +s 0s ) ↔ 𝑦 = 𝑥 ) )
21 20 rexbidva ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) ↔ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑦 = 𝑥 ) )
22 risset ⊢ ( 𝑥 ∈ ( L ‘ 𝑎 ) ↔ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑦 = 𝑥 )
23 21 22 bitr4di ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) ↔ 𝑥 ∈ ( L ‘ 𝑎 ) ) )
24 23 abbi1dv ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } = ( L ‘ 𝑎 ) )
25 rex0 ⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑧 = ( 𝑎 +s 𝑦 )
26 left0s ⊢ ( L ‘ 0s ) = ∅
27 26 rexeqi ⊢ ( ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) ↔ ∃ 𝑦 ∈ ∅ 𝑧 = ( 𝑎 +s 𝑦 ) )
28 25 27 mtbir ⊢ ¬ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 )
29 28 abf ⊢ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } = ∅
30 29 a1i ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } = ∅ )
31 24 30 uneq12d ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) = ( ( L ‘ 𝑎 ) ∪ ∅ ) )
32 un0 ⊢ ( ( L ‘ 𝑎 ) ∪ ∅ ) = ( L ‘ 𝑎 )
33 31 32 eqtrdi ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) = ( L ‘ 𝑎 ) )
34 elun2 ⊢ ( 𝑤 ∈ ( R ‘ 𝑎 ) → 𝑤 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) )
35 oveq1 ⊢ ( 𝑏 = 𝑤 → ( 𝑏 +s 0s ) = ( 𝑤 +s 0s ) )
36 id ⊢ ( 𝑏 = 𝑤 → 𝑏 = 𝑤 )
37 35 36 eqeq12d ⊢ ( 𝑏 = 𝑤 → ( ( 𝑏 +s 0s ) = 𝑏 ↔ ( 𝑤 +s 0s ) = 𝑤 ) )
38 37 rspcva ⊢ ( ( 𝑤 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( 𝑤 +s 0s ) = 𝑤 )
39 34 12 38 syl2anr ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑤 ∈ ( R ‘ 𝑎 ) ) → ( 𝑤 +s 0s ) = 𝑤 )
40 39 eqeq2d ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑤 ∈ ( R ‘ 𝑎 ) ) → ( 𝑥 = ( 𝑤 +s 0s ) ↔ 𝑥 = 𝑤 ) )
41 equcom ⊢ ( 𝑥 = 𝑤 ↔ 𝑤 = 𝑥 )
42 40 41 bitrdi ⊢ ( ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) ∧ 𝑤 ∈ ( R ‘ 𝑎 ) ) → ( 𝑥 = ( 𝑤 +s 0s ) ↔ 𝑤 = 𝑥 ) )
43 42 rexbidva ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) ↔ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑤 = 𝑥 ) )
44 risset ⊢ ( 𝑥 ∈ ( R ‘ 𝑎 ) ↔ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑤 = 𝑥 )
45 43 44 bitr4di ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) ↔ 𝑥 ∈ ( R ‘ 𝑎 ) ) )
46 45 abbi1dv ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } = ( R ‘ 𝑎 ) )
47 rex0 ⊢ ¬ ∃ 𝑤 ∈ ∅ 𝑧 = ( 𝑎 +s 𝑤 )
48 right0s ⊢ ( R ‘ 0s ) = ∅
49 48 rexeqi ⊢ ( ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) ↔ ∃ 𝑤 ∈ ∅ 𝑧 = ( 𝑎 +s 𝑤 ) )
50 47 49 mtbir ⊢ ¬ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 )
51 50 abf ⊢ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } = ∅
52 51 a1i ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } = ∅ )
53 46 52 uneq12d ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) = ( ( R ‘ 𝑎 ) ∪ ∅ ) )
54 un0 ⊢ ( ( R ‘ 𝑎 ) ∪ ∅ ) = ( R ‘ 𝑎 )
55 53 54 eqtrdi ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) = ( R ‘ 𝑎 ) )
56 33 55 oveq12d ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝑎 ) 𝑥 = ( 𝑦 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑦 ∈ ( L ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑤 ∈ ( R ‘ 𝑎 ) 𝑥 = ( 𝑤 +s 0s ) } ∪ { 𝑧 ∣ ∃ 𝑤 ∈ ( R ‘ 0s ) 𝑧 = ( 𝑎 +s 𝑤 ) } ) ) = ( ( L ‘ 𝑎 ) |s ( R ‘ 𝑎 ) ) )
57 lrcut ⊢ ( 𝑎 ∈ No → ( ( L ‘ 𝑎 ) |s ( R ‘ 𝑎 ) ) = 𝑎 )
58 57 adantr ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( ( L ‘ 𝑎 ) |s ( R ‘ 𝑎 ) ) = 𝑎 )
59 10 56 58 3eqtrd ⊢ ( ( 𝑎 ∈ No ∧ ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 ) → ( 𝑎 +s 0s ) = 𝑎 )
60 59 ex ⊢ ( 𝑎 ∈ No → ( ∀ 𝑏 ∈ ( ( L ‘ 𝑎 ) ∪ ( R ‘ 𝑎 ) ) ( 𝑏 +s 0s ) = 𝑏 → ( 𝑎 +s 0s ) = 𝑎 ) )
61 3 6 60 noinds ⊢ ( 𝐴 ∈ No → ( 𝐴 +s 0s ) = 𝐴 )