Theorem addsunif

Description: Uniformity theorem for surreal addition. This theorem states that we can use any cuts that define A and B in the definition of surreal addition. Theorem 3.2 of Gonshor p. 15. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsunif.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
	addsunif.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
	addsunif.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
	addsunif.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
Assertion	addsunif	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		addsunif.1	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
2		addsunif.2	⊢ ( 𝜑 → 𝑀 <<s 𝑆 )
3		addsunif.3	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
4		addsunif.4	⊢ ( 𝜑 → 𝐵 = ( 𝑀 |s 𝑆 ) )
5	1 2 3 4	addsuniflem	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) } ) |s ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) } ) ) )
6		oveq1	⊢ ( 𝑙 = 𝑏 → ( 𝑙 +s 𝐵 ) = ( 𝑏 +s 𝐵 ) )
7	6	eqeq2d	⊢ ( 𝑙 = 𝑏 → ( 𝑦 = ( 𝑙 +s 𝐵 ) ↔ 𝑦 = ( 𝑏 +s 𝐵 ) ) )
8	7	cbvrexvw	⊢ ( ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐿 𝑦 = ( 𝑏 +s 𝐵 ) )
9		eqeq1	⊢ ( 𝑦 = 𝑎 → ( 𝑦 = ( 𝑏 +s 𝐵 ) ↔ 𝑎 = ( 𝑏 +s 𝐵 ) ) )
10	9	rexbidv	⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑏 ∈ 𝐿 𝑦 = ( 𝑏 +s 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) ) )
11	8 10	bitrid	⊢ ( 𝑦 = 𝑎 → ( ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) ↔ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) ) )
12	11	cbvabv	⊢ { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) }
13		oveq2	⊢ ( 𝑚 = 𝑑 → ( 𝐴 +s 𝑚 ) = ( 𝐴 +s 𝑑 ) )
14	13	eqeq2d	⊢ ( 𝑚 = 𝑑 → ( 𝑧 = ( 𝐴 +s 𝑚 ) ↔ 𝑧 = ( 𝐴 +s 𝑑 ) ) )
15	14	cbvrexvw	⊢ ( ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) ↔ ∃ 𝑑 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑑 ) )
16		eqeq1	⊢ ( 𝑧 = 𝑐 → ( 𝑧 = ( 𝐴 +s 𝑑 ) ↔ 𝑐 = ( 𝐴 +s 𝑑 ) ) )
17	16	rexbidv	⊢ ( 𝑧 = 𝑐 → ( ∃ 𝑑 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑑 ) ↔ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) ) )
18	15 17	bitrid	⊢ ( 𝑧 = 𝑐 → ( ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) ↔ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) ) )
19	18	cbvabv	⊢ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } = { 𝑐 ∣ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) }
20	12 19	uneq12i	⊢ ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) = ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) } )
21		oveq1	⊢ ( 𝑟 = 𝑓 → ( 𝑟 +s 𝐵 ) = ( 𝑓 +s 𝐵 ) )
22	21	eqeq2d	⊢ ( 𝑟 = 𝑓 → ( 𝑤 = ( 𝑟 +s 𝐵 ) ↔ 𝑤 = ( 𝑓 +s 𝐵 ) ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) ↔ ∃ 𝑓 ∈ 𝑅 𝑤 = ( 𝑓 +s 𝐵 ) )
24		eqeq1	⊢ ( 𝑤 = 𝑒 → ( 𝑤 = ( 𝑓 +s 𝐵 ) ↔ 𝑒 = ( 𝑓 +s 𝐵 ) ) )
25	24	rexbidv	⊢ ( 𝑤 = 𝑒 → ( ∃ 𝑓 ∈ 𝑅 𝑤 = ( 𝑓 +s 𝐵 ) ↔ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) ) )
26	23 25	bitrid	⊢ ( 𝑤 = 𝑒 → ( ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) ↔ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) ) )
27	26	cbvabv	⊢ { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } = { 𝑒 ∣ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) }
28		oveq2	⊢ ( 𝑠 = ℎ → ( 𝐴 +s 𝑠 ) = ( 𝐴 +s ℎ ) )
29	28	eqeq2d	⊢ ( 𝑠 = ℎ → ( 𝑡 = ( 𝐴 +s 𝑠 ) ↔ 𝑡 = ( 𝐴 +s ℎ ) ) )
30	29	cbvrexvw	⊢ ( ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) ↔ ∃ ℎ ∈ 𝑆 𝑡 = ( 𝐴 +s ℎ ) )
31		eqeq1	⊢ ( 𝑡 = 𝑔 → ( 𝑡 = ( 𝐴 +s ℎ ) ↔ 𝑔 = ( 𝐴 +s ℎ ) ) )
32	31	rexbidv	⊢ ( 𝑡 = 𝑔 → ( ∃ ℎ ∈ 𝑆 𝑡 = ( 𝐴 +s ℎ ) ↔ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) ) )
33	30 32	bitrid	⊢ ( 𝑡 = 𝑔 → ( ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) ↔ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) ) )
34	33	cbvabv	⊢ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } = { 𝑔 ∣ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) }
35	27 34	uneq12i	⊢ ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) = ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) } )
36	20 35	oveq12i	⊢ ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) = ( ( { 𝑎 ∣ ∃ 𝑏 ∈ 𝐿 𝑎 = ( 𝑏 +s 𝐵 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ 𝑀 𝑐 = ( 𝐴 +s 𝑑 ) } ) |s ( { 𝑒 ∣ ∃ 𝑓 ∈ 𝑅 𝑒 = ( 𝑓 +s 𝐵 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ 𝑆 𝑔 = ( 𝐴 +s ℎ ) } ) )
37	5 36	eqtr4di	⊢ ( 𝜑 → ( 𝐴 +s 𝐵 ) = ( ( { 𝑦 ∣ ∃ 𝑙 ∈ 𝐿 𝑦 = ( 𝑙 +s 𝐵 ) } ∪ { 𝑧 ∣ ∃ 𝑚 ∈ 𝑀 𝑧 = ( 𝐴 +s 𝑚 ) } ) |s ( { 𝑤 ∣ ∃ 𝑟 ∈ 𝑅 𝑤 = ( 𝑟 +s 𝐵 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ 𝑆 𝑡 = ( 𝐴 +s 𝑠 ) } ) ) )