Theorem onaddscl

Description: The surreal ordinals are closed under addition. (Contributed by Scott Fenton, 22-Aug-2025)

	Ref	Expression
Assertion	onaddscl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 +s 𝐵 ) ∈ Ons )

Proof

Step	Hyp	Ref	Expression
1		fvex	⊢ ( L ‘ 𝐴 ) ∈ V
2	1	abrexex	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∈ V
3		fvex	⊢ ( L ‘ 𝐵 ) ∈ V
4	3	abrexex	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ∈ V
5	2 4	unex	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) ∈ V
6	5	a1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) ∈ V )
7		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
8	7	sseli	⊢ ( 𝑦 ∈ ( L ‘ 𝐴 ) → 𝑦 ∈ No )
9	8	adantl	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → 𝑦 ∈ No )
10		onsno	⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
11	10	ad2antlr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → 𝐵 ∈ No )
12	9 11	addscld	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → ( 𝑦 +s 𝐵 ) ∈ No )
13		eleq1	⊢ ( 𝑥 = ( 𝑦 +s 𝐵 ) → ( 𝑥 ∈ No ↔ ( 𝑦 +s 𝐵 ) ∈ No ) )
14	12 13	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → ( 𝑥 = ( 𝑦 +s 𝐵 ) → 𝑥 ∈ No ) )
15	14	rexlimdva	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) → 𝑥 ∈ No ) )
16	15	abssdv	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ⊆ No )
17		onsno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
18	17	ad2antrr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → 𝐴 ∈ No )
19		leftssno	⊢ ( L ‘ 𝐵 ) ⊆ No
20	19	sseli	⊢ ( 𝑦 ∈ ( L ‘ 𝐵 ) → 𝑦 ∈ No )
21	20	adantl	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → 𝑦 ∈ No )
22	18 21	addscld	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 +s 𝑦 ) ∈ No )
23		eleq1	⊢ ( 𝑥 = ( 𝐴 +s 𝑦 ) → ( 𝑥 ∈ No ↔ ( 𝐴 +s 𝑦 ) ∈ No ) )
24	22 23	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → ( 𝑥 = ( 𝐴 +s 𝑦 ) → 𝑥 ∈ No ) )
25	24	rexlimdva	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) → 𝑥 ∈ No ) )
26	25	abssdv	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ⊆ No )
27	16 26	unssd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) ⊆ No )
28	1	elpw	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
29	7 28	mpbir	⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
30		nulssgt	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No → ( L ‘ 𝐴 ) <<s ∅ )
31	29 30	mp1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐴 ) <<s ∅ )
32	3	elpw	⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No ↔ ( L ‘ 𝐵 ) ⊆ No )
33	19 32	mpbir	⊢ ( L ‘ 𝐵 ) ∈ 𝒫 No
34		nulssgt	⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No → ( L ‘ 𝐵 ) <<s ∅ )
35	33 34	mp1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐵 ) <<s ∅ )
36		onscutleft	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
37	36	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
38		onscutleft	⊢ ( 𝐵 ∈ Ons → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
39	38	adantl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
40	31 35 37 39	addsunif	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 ) } ) ) )
41		rex0	⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 )
42	41	abf	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 ) } = ∅
43		rex0	⊢ ¬ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 )
44	43	abf	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 ) } = ∅
45	42 44	uneq12i	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 ) } ) = ( ∅ ∪ ∅ )
46		un0	⊢ ( ∅ ∪ ∅ ) = ∅
47	45 46	eqtri	⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 ) } ) = ∅
48	47	oveq2i	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) |s ( { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ∅ 𝑥 = ( 𝐴 +s 𝑦 ) } ) ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) |s ∅ )
49	40 48	eqtrdi	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 +s 𝐵 ) = ( ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) |s ∅ ) )
50	6 27 49	elons2d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 +s 𝐵 ) ∈ Ons )