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		leftno	⊢ ( 𝑦 ∈ ( L ‘ 𝐴 ) → 𝑦 ∈ No )
8	7	adantl	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → 𝑦 ∈ No )
9		onno	⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
10	9	ad2antlr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → 𝐵 ∈ No )
11	8 10	addscld	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → ( 𝑦 +s 𝐵 ) ∈ No )
12		eleq1	⊢ ( 𝑥 = ( 𝑦 +s 𝐵 ) → ( 𝑥 ∈ No ↔ ( 𝑦 +s 𝐵 ) ∈ No ) )
13	11 12	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐴 ) ) → ( 𝑥 = ( 𝑦 +s 𝐵 ) → 𝑥 ∈ No ) )
14	13	rexlimdva	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) → 𝑥 ∈ No ) )
15	14	abssdv	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ⊆ No )
16		onno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
17	16	ad2antrr	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → 𝐴 ∈ No )
18		leftno	⊢ ( 𝑦 ∈ ( L ‘ 𝐵 ) → 𝑦 ∈ No )
19	18	adantl	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → 𝑦 ∈ No )
20	17 19	addscld	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → ( 𝐴 +s 𝑦 ) ∈ No )
21		eleq1	⊢ ( 𝑥 = ( 𝐴 +s 𝑦 ) → ( 𝑥 ∈ No ↔ ( 𝐴 +s 𝑦 ) ∈ No ) )
22	20 21	syl5ibrcom	⊢ ( ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) ∧ 𝑦 ∈ ( L ‘ 𝐵 ) ) → ( 𝑥 = ( 𝐴 +s 𝑦 ) → 𝑥 ∈ No ) )
23	22	rexlimdva	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) → 𝑥 ∈ No ) )
24	23	abssdv	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ⊆ No )
25	15 24	unssd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐴 ) 𝑥 = ( 𝑦 +s 𝐵 ) } ∪ { 𝑥 ∣ ∃ 𝑦 ∈ ( L ‘ 𝐵 ) 𝑥 = ( 𝐴 +s 𝑦 ) } ) ⊆ No )
26		leftssno	⊢ ( L ‘ 𝐴 ) ⊆ No
27	1	elpw	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No ↔ ( L ‘ 𝐴 ) ⊆ No )
28	26 27	mpbir	⊢ ( L ‘ 𝐴 ) ∈ 𝒫 No
29		nulsgts	⊢ ( ( L ‘ 𝐴 ) ∈ 𝒫 No → ( L ‘ 𝐴 ) <<s ∅ )
30	28 29	mp1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐴 ) <<s ∅ )
31		leftssno	⊢ ( L ‘ 𝐵 ) ⊆ No
32	3	elpw	⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No ↔ ( L ‘ 𝐵 ) ⊆ No )
33	31 32	mpbir	⊢ ( L ‘ 𝐵 ) ∈ 𝒫 No
34		nulsgts	⊢ ( ( L ‘ 𝐵 ) ∈ 𝒫 No → ( L ‘ 𝐵 ) <<s ∅ )
35	33 34	mp1i	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( L ‘ 𝐵 ) <<s ∅ )
36		oncutleft	⊢ ( 𝐴 ∈ Ons → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
37	36	adantr	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐴 = ( ( L ‘ 𝐴 ) |s ∅ ) )
38		oncutleft	⊢ ( 𝐵 ∈ Ons → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
39	38	adantl	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝐵 = ( ( L ‘ 𝐵 ) |s ∅ ) )
40	30 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 25 49	elons2d	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( 𝐴 +s 𝐵 ) ∈ Ons )