Theorem addsval2

Description: The value of surreal addition with different choices for each bound variable. Definition from Conway p. 5. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Assertion	addsval2	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsval	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) } ) ) )
2		eqeq1	⊢ ( 𝑎 = 𝑦 → ( 𝑎 = ( 𝑏 +s 𝐵 ) ↔ 𝑦 = ( 𝑏 +s 𝐵 ) ) )
3	2	rexbidv	⊢ ( 𝑎 = 𝑦 → ( ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) ↔ ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑏 +s 𝐵 ) ) )
4		oveq1	⊢ ( 𝑏 = 𝑙 → ( 𝑏 +s 𝐵 ) = ( 𝑙 +s 𝐵 ) )
5	4	eqeq2d	⊢ ( 𝑏 = 𝑙 → ( 𝑦 = ( 𝑏 +s 𝐵 ) ↔ 𝑦 = ( 𝑙 +s 𝐵 ) ) )
6	5	cbvrexvw	⊢ ( ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑏 +s 𝐵 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) )
7	3 6	bitrdi	⊢ ( 𝑎 = 𝑦 → ( ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) ) )
8	7	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) } = { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) }
9		eqeq1	⊢ ( 𝑐 = 𝑧 → ( 𝑐 = ( 𝐴 +s 𝑏 ) ↔ 𝑧 = ( 𝐴 +s 𝑏 ) ) )
10	9	rexbidv	⊢ ( 𝑐 = 𝑧 → ( ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) ↔ ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑏 ) ) )
11		oveq2	⊢ ( 𝑏 = 𝑚 → ( 𝐴 +s 𝑏 ) = ( 𝐴 +s 𝑚 ) )
12	11	eqeq2d	⊢ ( 𝑏 = 𝑚 → ( 𝑧 = ( 𝐴 +s 𝑏 ) ↔ 𝑧 = ( 𝐴 +s 𝑚 ) ) )
13	12	cbvrexvw	⊢ ( ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑏 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) )
14	10 13	bitrdi	⊢ ( 𝑐 = 𝑧 → ( ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) ) )
15	14	cbvabv	⊢ { 𝑐 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) } = { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) }
16	8 15	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) } ) = ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) } )
17		eqeq1	⊢ ( 𝑎 = 𝑤 → ( 𝑎 = ( 𝑑 +s 𝐵 ) ↔ 𝑤 = ( 𝑑 +s 𝐵 ) ) )
18	17	rexbidv	⊢ ( 𝑎 = 𝑤 → ( ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) ↔ ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑑 +s 𝐵 ) ) )
19		oveq1	⊢ ( 𝑑 = 𝑟 → ( 𝑑 +s 𝐵 ) = ( 𝑟 +s 𝐵 ) )
20	19	eqeq2d	⊢ ( 𝑑 = 𝑟 → ( 𝑤 = ( 𝑑 +s 𝐵 ) ↔ 𝑤 = ( 𝑟 +s 𝐵 ) ) )
21	20	cbvrexvw	⊢ ( ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑑 +s 𝐵 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) )
22	18 21	bitrdi	⊢ ( 𝑎 = 𝑤 → ( ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) ) )
23	22	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) } = { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) }
24		eqeq1	⊢ ( 𝑐 = 𝑡 → ( 𝑐 = ( 𝐴 +s 𝑑 ) ↔ 𝑡 = ( 𝐴 +s 𝑑 ) ) )
25	24	rexbidv	⊢ ( 𝑐 = 𝑡 → ( ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) ↔ ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑑 ) ) )
26		oveq2	⊢ ( 𝑑 = 𝑠 → ( 𝐴 +s 𝑑 ) = ( 𝐴 +s 𝑠 ) )
27	26	eqeq2d	⊢ ( 𝑑 = 𝑠 → ( 𝑡 = ( 𝐴 +s 𝑑 ) ↔ 𝑡 = ( 𝐴 +s 𝑠 ) ) )
28	27	cbvrexvw	⊢ ( ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑑 ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) )
29	25 28	bitrdi	⊢ ( 𝑐 = 𝑡 → ( ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) ) )
30	29	cbvabv	⊢ { 𝑐 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) } = { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) }
31	23 30	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) } ) = ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) } )
32	16 31	oveq12i	⊢ ( ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐴 ) 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑏 ∈ ( L ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑏 ) } ) |s ( { 𝑎 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐴 ) 𝑎 = ( 𝑑 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( R ‘ 𝐵 ) 𝑐 = ( 𝐴 +s 𝑑 ) } ) ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) } ) )
33	1 32	eqtrdi	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ ( L ‘ 𝐴 ) 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ ( L ‘ 𝐵 ) 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝐴 ) 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝐵 ) 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )