Metamath Proof Explorer

Theorem addscom

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

Ref Expression
Assertion addscom ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( 𝐵 +s 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 𝑥O → ( 𝑥 +s 𝑦 ) = ( 𝑥O +s 𝑦 ) )
2 oveq2 ⊢ ( 𝑥 = 𝑥O → ( 𝑦 +s 𝑥 ) = ( 𝑦 +s 𝑥O ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 𝑥O → ( ( 𝑥 +s 𝑦 ) = ( 𝑦 +s 𝑥 ) ↔ ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ) )
4 oveq2 ⊢ ( 𝑦 = 𝑦O → ( 𝑥O +s 𝑦 ) = ( 𝑥O +s 𝑦O ) )
5 oveq1 ⊢ ( 𝑦 = 𝑦O → ( 𝑦 +s 𝑥O ) = ( 𝑦O +s 𝑥O ) )
6 4 5 eqeq12d ⊢ ( 𝑦 = 𝑦O → ( ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ↔ ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ) )
7 oveq1 ⊢ ( 𝑥 = 𝑥O → ( 𝑥 +s 𝑦O ) = ( 𝑥O +s 𝑦O ) )
8 oveq2 ⊢ ( 𝑥 = 𝑥O → ( 𝑦O +s 𝑥 ) = ( 𝑦O +s 𝑥O ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = 𝑥O → ( ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ↔ ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ) )
10 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +s 𝑦 ) = ( 𝐴 +s 𝑦 ) )
11 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 +s 𝑥 ) = ( 𝑦 +s 𝐴 ) )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 +s 𝑦 ) = ( 𝑦 +s 𝑥 ) ↔ ( 𝐴 +s 𝑦 ) = ( 𝑦 +s 𝐴 ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s 𝑦 ) = ( 𝐴 +s 𝐵 ) )
14 oveq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 +s 𝐴 ) = ( 𝐵 +s 𝐴 ) )
15 13 14 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 +s 𝑦 ) = ( 𝑦 +s 𝐴 ) ↔ ( 𝐴 +s 𝐵 ) = ( 𝐵 +s 𝐴 ) ) )
16 simpr2 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) )
17 elun1 ⊢ ( 𝑙 ∈ ( L ‘ 𝑥 ) → 𝑙 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
18 oveq1 ⊢ ( 𝑥O = 𝑙 → ( 𝑥O +s 𝑦 ) = ( 𝑙 +s 𝑦 ) )
19 oveq2 ⊢ ( 𝑥O = 𝑙 → ( 𝑦 +s 𝑥O ) = ( 𝑦 +s 𝑙 ) )
20 18 19 eqeq12d ⊢ ( 𝑥O = 𝑙 → ( ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ↔ ( 𝑙 +s 𝑦 ) = ( 𝑦 +s 𝑙 ) ) )
21 20 rspccva ⊢ ( ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ 𝑙 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑙 +s 𝑦 ) = ( 𝑦 +s 𝑙 ) )
22 16 17 21 syl2an ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑙 ∈ ( L ‘ 𝑥 ) ) → ( 𝑙 +s 𝑦 ) = ( 𝑦 +s 𝑙 ) )
23 22 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑙 ∈ ( L ‘ 𝑥 ) ) → ( 𝑤 = ( 𝑙 +s 𝑦 ) ↔ 𝑤 = ( 𝑦 +s 𝑙 ) ) )
24 23 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) ) )
25 24 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } = { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } )
26 simpr3 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) )
27 elun1 ⊢ ( 𝑙 ∈ ( L ‘ 𝑦 ) → 𝑙 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
28 oveq2 ⊢ ( 𝑦O = 𝑙 → ( 𝑥 +s 𝑦O ) = ( 𝑥 +s 𝑙 ) )
29 oveq1 ⊢ ( 𝑦O = 𝑙 → ( 𝑦O +s 𝑥 ) = ( 𝑙 +s 𝑥 ) )
30 28 29 eqeq12d ⊢ ( 𝑦O = 𝑙 → ( ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ↔ ( 𝑥 +s 𝑙 ) = ( 𝑙 +s 𝑥 ) ) )
31 30 rspccva ⊢ ( ( ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ∧ 𝑙 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( 𝑥 +s 𝑙 ) = ( 𝑙 +s 𝑥 ) )
32 26 27 31 syl2an ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑙 ∈ ( L ‘ 𝑦 ) ) → ( 𝑥 +s 𝑙 ) = ( 𝑙 +s 𝑥 ) )
33 32 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑙 ∈ ( L ‘ 𝑦 ) ) → ( 𝑧 = ( 𝑥 +s 𝑙 ) ↔ 𝑧 = ( 𝑙 +s 𝑥 ) ) )
34 33 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) ) )
35 34 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } = { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } )
36 25 35 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } ) = ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ) )
37 uncom ⊢ ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ) = ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } )
38 36 37 eqtrdi ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } ) = ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ) )
39 elun2 ⊢ ( 𝑟 ∈ ( R ‘ 𝑥 ) → 𝑟 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
40 oveq1 ⊢ ( 𝑥O = 𝑟 → ( 𝑥O +s 𝑦 ) = ( 𝑟 +s 𝑦 ) )
41 oveq2 ⊢ ( 𝑥O = 𝑟 → ( 𝑦 +s 𝑥O ) = ( 𝑦 +s 𝑟 ) )
42 40 41 eqeq12d ⊢ ( 𝑥O = 𝑟 → ( ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ↔ ( 𝑟 +s 𝑦 ) = ( 𝑦 +s 𝑟 ) ) )
43 42 rspccva ⊢ ( ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ 𝑟 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑟 +s 𝑦 ) = ( 𝑦 +s 𝑟 ) )
44 16 39 43 syl2an ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑟 ∈ ( R ‘ 𝑥 ) ) → ( 𝑟 +s 𝑦 ) = ( 𝑦 +s 𝑟 ) )
45 44 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑟 ∈ ( R ‘ 𝑥 ) ) → ( 𝑤 = ( 𝑟 +s 𝑦 ) ↔ 𝑤 = ( 𝑦 +s 𝑟 ) ) )
46 45 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) ) )
47 46 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } = { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } )
48 elun2 ⊢ ( 𝑟 ∈ ( R ‘ 𝑦 ) → 𝑟 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
49 oveq2 ⊢ ( 𝑦O = 𝑟 → ( 𝑥 +s 𝑦O ) = ( 𝑥 +s 𝑟 ) )
50 oveq1 ⊢ ( 𝑦O = 𝑟 → ( 𝑦O +s 𝑥 ) = ( 𝑟 +s 𝑥 ) )
51 49 50 eqeq12d ⊢ ( 𝑦O = 𝑟 → ( ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ↔ ( 𝑥 +s 𝑟 ) = ( 𝑟 +s 𝑥 ) ) )
52 51 rspccva ⊢ ( ( ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ∧ 𝑟 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( 𝑥 +s 𝑟 ) = ( 𝑟 +s 𝑥 ) )
53 26 48 52 syl2an ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑟 ∈ ( R ‘ 𝑦 ) ) → ( 𝑥 +s 𝑟 ) = ( 𝑟 +s 𝑥 ) )
54 53 eqeq2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) ∧ 𝑟 ∈ ( R ‘ 𝑦 ) ) → ( 𝑧 = ( 𝑥 +s 𝑟 ) ↔ 𝑧 = ( 𝑟 +s 𝑥 ) ) )
55 54 rexbidva ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) ) )
56 55 abbidv ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } = { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } )
57 47 56 uneq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } ) = ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ) )
58 uncom ⊢ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ) = ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } )
59 57 58 eqtrdi ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } ) = ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ) )
60 38 59 oveq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } ) ) = ( ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ) |s ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ) ) )
61 addsov ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( 𝑥 +s 𝑦 ) = ( ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } ) ) )
62 61 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( 𝑥 +s 𝑦 ) = ( ( { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑙 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑙 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑟 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑟 ) } ) ) )
63 addsov ⊢ ( ( 𝑦 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑦 +s 𝑥 ) = ( ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ) |s ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ) ) )
64 63 ancoms ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( 𝑦 +s 𝑥 ) = ( ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ) |s ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ) ) )
65 64 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( 𝑦 +s 𝑥 ) = ( ( { 𝑧 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑙 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑙 ) } ) |s ( { 𝑧 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑟 +s 𝑥 ) } ∪ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) 𝑤 = ( 𝑦 +s 𝑟 ) } ) ) )
66 60 62 65 3eqtr4d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) ) → ( 𝑥 +s 𝑦 ) = ( 𝑦 +s 𝑥 ) )
67 66 ex ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥O +s 𝑦O ) = ( 𝑦O +s 𝑥O ) ∧ ∀ 𝑥O ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( 𝑥O +s 𝑦 ) = ( 𝑦 +s 𝑥O ) ∧ ∀ 𝑦O ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( 𝑥 +s 𝑦O ) = ( 𝑦O +s 𝑥 ) ) → ( 𝑥 +s 𝑦 ) = ( 𝑦 +s 𝑥 ) ) )
68 3 6 9 12 15 67 no2inds ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( 𝐵 +s 𝐴 ) )