Theorem addscut

Description: Demonstrate the cut properties of surreal addition. This gives us closure together with a pair of set-less-than relationships for surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addscut.1	⊢ ( 𝜑 → 𝑋 ∈ No )
	addscut.2	⊢ ( 𝜑 → 𝑌 ∈ No )
Assertion	addscut	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		addscut.1	⊢ ( 𝜑 → 𝑋 ∈ No )
2		addscut.2	⊢ ( 𝜑 → 𝑌 ∈ No )
3	1 2	addscutlem	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) ) )
4		biid	⊢ ( ( 𝑋 +s 𝑌 ) ∈ No ↔ ( 𝑋 +s 𝑌 ) ∈ No )
5		oveq1	⊢ ( 𝑙 = 𝑏 → ( 𝑙 +s 𝑌 ) = ( 𝑏 +s 𝑌 ) )
6	5	eqeq2d	⊢ ( 𝑙 = 𝑏 → ( 𝑝 = ( 𝑙 +s 𝑌 ) ↔ 𝑝 = ( 𝑏 +s 𝑌 ) ) )
7	6	cbvrexvw	⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) ↔ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑏 +s 𝑌 ) )
8		eqeq1	⊢ ( 𝑝 = 𝑎 → ( 𝑝 = ( 𝑏 +s 𝑌 ) ↔ 𝑎 = ( 𝑏 +s 𝑌 ) ) )
9	8	rexbidv	⊢ ( 𝑝 = 𝑎 → ( ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑏 +s 𝑌 ) ↔ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) ) )
10	7 9	bitrid	⊢ ( 𝑝 = 𝑎 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) ↔ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) ) )
11	10	cbvabv	⊢ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } = { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) }
12		oveq2	⊢ ( 𝑚 = 𝑑 → ( 𝑋 +s 𝑚 ) = ( 𝑋 +s 𝑑 ) )
13	12	eqeq2d	⊢ ( 𝑚 = 𝑑 → ( 𝑞 = ( 𝑋 +s 𝑚 ) ↔ 𝑞 = ( 𝑋 +s 𝑑 ) ) )
14	13	cbvrexvw	⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑑 ) )
15		eqeq1	⊢ ( 𝑞 = 𝑐 → ( 𝑞 = ( 𝑋 +s 𝑑 ) ↔ 𝑐 = ( 𝑋 +s 𝑑 ) ) )
16	15	rexbidv	⊢ ( 𝑞 = 𝑐 → ( ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑑 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) ) )
17	14 16	bitrid	⊢ ( 𝑞 = 𝑐 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) ↔ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) ) )
18	17	cbvabv	⊢ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } = { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) }
19	11 18	uneq12i	⊢ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) = ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) } )
20	19	breq1i	⊢ ( ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ↔ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑌 ) } )
21		oveq1	⊢ ( 𝑟 = 𝑓 → ( 𝑟 +s 𝑌 ) = ( 𝑓 +s 𝑌 ) )
22	21	eqeq2d	⊢ ( 𝑟 = 𝑓 → ( 𝑤 = ( 𝑟 +s 𝑌 ) ↔ 𝑤 = ( 𝑓 +s 𝑌 ) ) )
23	22	cbvrexvw	⊢ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) ↔ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑓 +s 𝑌 ) )
24		eqeq1	⊢ ( 𝑤 = 𝑒 → ( 𝑤 = ( 𝑓 +s 𝑌 ) ↔ 𝑒 = ( 𝑓 +s 𝑌 ) ) )
25	24	rexbidv	⊢ ( 𝑤 = 𝑒 → ( ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑓 +s 𝑌 ) ↔ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) ) )
26	23 25	bitrid	⊢ ( 𝑤 = 𝑒 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) ↔ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) ) )
27	26	cbvabv	⊢ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } = { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) }
28		oveq2	⊢ ( 𝑠 = ℎ → ( 𝑋 +s 𝑠 ) = ( 𝑋 +s ℎ ) )
29	28	eqeq2d	⊢ ( 𝑠 = ℎ → ( 𝑡 = ( 𝑋 +s 𝑠 ) ↔ 𝑡 = ( 𝑋 +s ℎ ) ) )
30	29	cbvrexvw	⊢ ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) ↔ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s ℎ ) )
31		eqeq1	⊢ ( 𝑡 = 𝑔 → ( 𝑡 = ( 𝑋 +s ℎ ) ↔ 𝑔 = ( 𝑋 +s ℎ ) ) )
32	31	rexbidv	⊢ ( 𝑡 = 𝑔 → ( ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s ℎ ) ↔ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) ) )
33	30 32	bitrid	⊢ ( 𝑡 = 𝑔 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) ↔ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) ) )
34	33	cbvabv	⊢ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } = { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) }
35	27 34	uneq12i	⊢ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) = ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } )
36	35	breq2i	⊢ ( { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) )
37	4 20 36	3anbi123i	⊢ ( ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑎 ∣ ∃ 𝑏 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑏 +s 𝑌 ) } ∪ { 𝑐 ∣ ∃ 𝑑 ∈ ( L ‘ 𝑌 ) 𝑐 = ( 𝑋 +s 𝑑 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑒 ∣ ∃ 𝑓 ∈ ( R ‘ 𝑋 ) 𝑒 = ( 𝑓 +s 𝑌 ) } ∪ { 𝑔 ∣ ∃ ℎ ∈ ( R ‘ 𝑌 ) 𝑔 = ( 𝑋 +s ℎ ) } ) ) )
38	3 37	sylibr	⊢ ( 𝜑 → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s { ( 𝑋 +s 𝑌 ) } ∧ { ( 𝑋 +s 𝑌 ) } <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) )