Theorem addsonbday

Description: The birthday of the sum of two ordinals is the natural sum of their birthdays. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Assertion	addsonbday	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onsno	⊢ ( 𝐴 ∈ Ons → 𝐴 ∈ No )
2		onsno	⊢ ( 𝐵 ∈ Ons → 𝐵 ∈ No )
3		addsbday	⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
5		fveq2	⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑥𝑂 ) )
6	5	oveq1d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) )
7		fvoveq1	⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) )
8	6 7	sseq12d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) )
9		fveq2	⊢ ( 𝑦 = 𝑦𝑂 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑦𝑂 ) )
10	9	oveq2d	⊢ ( 𝑦 = 𝑦𝑂 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) )
11		oveq2	⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 +s 𝑦 ) = ( 𝑥𝑂 +s 𝑦𝑂 ) )
12	11	fveq2d	⊢ ( 𝑦 = 𝑦𝑂 → ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) )
13	10 12	sseq12d	⊢ ( 𝑦 = 𝑦𝑂 → ( ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) )
14	5	oveq1d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) )
15		fvoveq1	⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) )
16	14 15	sseq12d	⊢ ( 𝑥 = 𝑥𝑂 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ↔ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) )
17		fveq2	⊢ ( 𝑥 = 𝐴 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝐴 ) )
18	17	oveq1d	⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) )
19		fvoveq1	⊢ ( 𝑥 = 𝐴 → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( 𝐴 +s 𝑦 ) ) )
20	18 19	sseq12d	⊢ ( 𝑥 = 𝐴 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝐴 +s 𝑦 ) ) ) )
21		fveq2	⊢ ( 𝑦 = 𝐵 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝐵 ) )
22	21	oveq2d	⊢ ( 𝑦 = 𝐵 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
23		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s 𝑦 ) = ( 𝐴 +s 𝐵 ) )
24	23	fveq2d	⊢ ( 𝑦 = 𝐵 → ( bday ‘ ( 𝐴 +s 𝑦 ) ) = ( bday ‘ ( 𝐴 +s 𝐵 ) ) )
25	22 24	sseq12d	⊢ ( 𝑦 = 𝐵 → ( ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝐴 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ⊆ ( bday ‘ ( 𝐴 +s 𝐵 ) ) ) )
26		bdayelon	⊢ ( bday ‘ 𝑥 ) ∈ On
27		bdayelon	⊢ ( bday ‘ 𝑦 ) ∈ On
28		naddov2	⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝑦 ) ∈ On ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ∩ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } )
29	26 27 28	mp2an	⊢ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ∩ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) }
30	27	oneli	⊢ ( 𝑞 ∈ ( bday ‘ 𝑦 ) → 𝑞 ∈ On )
31		breq1	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( 𝑦𝑂 <s 𝑦 ↔ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ) )
32		fveq2	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( bday ‘ 𝑦𝑂 ) = ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) )
33	32	oveq2d	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) = ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) )
34		oveq2	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( 𝑥 +s 𝑦𝑂 ) = ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) )
35	34	fveq2d	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) = ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) )
36	33 35	sseq12d	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ↔ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ) )
37	31 36	imbi12d	⊢ ( 𝑦𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) → ( ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ↔ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ) ) )
38		simplr3	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) )
39		onsiso	⊢ ( bday ↾ Ons ) Isom <s , E ( Ons , On )
40		isof1o	⊢ ( ( bday ↾ Ons ) Isom <s , E ( Ons , On ) → ( bday ↾ Ons ) : Ons –1-1-onto→ On )
41	39 40	ax-mp	⊢ ( bday ↾ Ons ) : Ons –1-1-onto→ On
42		f1ocnvdm	⊢ ( ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ∧ 𝑞 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons )
43	41 42	mpan	⊢ ( 𝑞 ∈ On → ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons )
44	43	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons )
45	37 38 44	rspcdva	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ) )
46	45	impr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑞 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) )
47		onsno	⊢ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons → ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ No )
48	44 47	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ No )
49		simpllr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → 𝑦 ∈ Ons )
50		onsno	⊢ ( 𝑦 ∈ Ons → 𝑦 ∈ No )
51	49 50	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → 𝑦 ∈ No )
52		simplll	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → 𝑥 ∈ Ons )
53		onsno	⊢ ( 𝑥 ∈ Ons → 𝑥 ∈ No )
54	52 53	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → 𝑥 ∈ No )
55	48 51 54	sltadd2d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ↔ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) <s ( 𝑥 +s 𝑦 ) ) )
56		onaddscl	⊢ ( ( 𝑥 ∈ Ons ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons ) → ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ Ons )
57	52 44 56	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ Ons )
58		onaddscl	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( 𝑥 +s 𝑦 ) ∈ Ons )
59	58	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( 𝑥 +s 𝑦 ) ∈ Ons )
60		onslt	⊢ ( ( ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ Ons ∧ ( 𝑥 +s 𝑦 ) ∈ Ons ) → ( ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) <s ( 𝑥 +s 𝑦 ) ↔ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
61	57 59 60	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) <s ( 𝑥 +s 𝑦 ) ↔ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
62	55 61	bitrd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ↔ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
63	62	biimpd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 → ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
64	63	impr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑞 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ) ) → ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
65		bdayelon	⊢ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ On
66		naddcl	⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ On ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ On )
67	26 65 66	mp2an	⊢ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ On
68	67	onordi	⊢ Ord ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) )
69		bdayelon	⊢ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ On
70	69	onordi	⊢ Ord ( bday ‘ ( 𝑥 +s 𝑦 ) )
71		ordtr2	⊢ ( ( Ord ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∧ Ord ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∧ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
72	68 70 71	mp2an	⊢ ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ⊆ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∧ ( bday ‘ ( 𝑥 +s ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
73	46 64 72	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑞 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
74	73	expr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
75	43	fvresd	⊢ ( 𝑞 ∈ On → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) = ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) )
76	75	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) = ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) )
77	76	oveq2d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) = ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) )
78	77	eleq1d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝑥 ) +no ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
79	74 78	sylibrd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
80		onslt	⊢ ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ↔ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ ( bday ‘ 𝑦 ) ) )
81	44 49 80	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ↔ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ ( bday ‘ 𝑦 ) ) )
82		f1ocnvfv2	⊢ ( ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ∧ 𝑞 ∈ On ) → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) = 𝑞 )
83	41 82	mpan	⊢ ( 𝑞 ∈ On → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) = 𝑞 )
84	75 83	eqtr3d	⊢ ( 𝑞 ∈ On → ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) = 𝑞 )
85	84	eleq1d	⊢ ( 𝑞 ∈ On → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ ( bday ‘ 𝑦 ) ↔ 𝑞 ∈ ( bday ‘ 𝑦 ) ) )
86	85	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ∈ ( bday ‘ 𝑦 ) ↔ 𝑞 ∈ ( bday ‘ 𝑦 ) ) )
87	81 86	bitrd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) <s 𝑦 ↔ 𝑞 ∈ ( bday ‘ 𝑦 ) ) )
88	83	oveq2d	⊢ ( 𝑞 ∈ On → ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) = ( ( bday ‘ 𝑥 ) +no 𝑞 ) )
89	88	eleq1d	⊢ ( 𝑞 ∈ On → ( ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
90	89	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( ( ( bday ‘ 𝑥 ) +no ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑞 ) ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
91	79 87 90	3imtr3d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑞 ∈ On ) → ( 𝑞 ∈ ( bday ‘ 𝑦 ) → ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
92	91	ex	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑞 ∈ On → ( 𝑞 ∈ ( bday ‘ 𝑦 ) → ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
93	30 92	syl5	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑞 ∈ ( bday ‘ 𝑦 ) → ( 𝑞 ∈ ( bday ‘ 𝑦 ) → ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
94	93	pm2.43d	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑞 ∈ ( bday ‘ 𝑦 ) → ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
95	94	ralrimiv	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
96	26	oneli	⊢ ( 𝑝 ∈ ( bday ‘ 𝑥 ) → 𝑝 ∈ On )
97		breq1	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( 𝑥𝑂 <s 𝑥 ↔ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ) )
98		fveq2	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( bday ‘ 𝑥𝑂 ) = ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) )
99	98	oveq1d	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) )
100		fvoveq1	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) = ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) )
101	99 100	sseq12d	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ↔ ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ) )
102	97 101	imbi12d	⊢ ( 𝑥𝑂 = ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) → ( ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ↔ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ) ) )
103		simplr2	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) )
104		f1ocnvdm	⊢ ( ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ∧ 𝑝 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons )
105	41 104	mpan	⊢ ( 𝑝 ∈ On → ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons )
106	105	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons )
107	102 103 106	rspcdva	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ) )
108	107	impr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑝 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ) ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) )
109		onsno	⊢ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons → ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ No )
110	106 109	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ No )
111		simplll	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → 𝑥 ∈ Ons )
112	111 53	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → 𝑥 ∈ No )
113		simpllr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → 𝑦 ∈ Ons )
114	113 50	syl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → 𝑦 ∈ No )
115	110 112 114	sltadd1d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) <s ( 𝑥 +s 𝑦 ) ) )
116		onaddscl	⊢ ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ∈ Ons )
117	106 113 116	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ∈ Ons )
118	58	ad2antrr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( 𝑥 +s 𝑦 ) ∈ Ons )
119		onslt	⊢ ( ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ∈ Ons ∧ ( 𝑥 +s 𝑦 ) ∈ Ons ) → ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) <s ( 𝑥 +s 𝑦 ) ↔ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
120	117 118 119	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) <s ( 𝑥 +s 𝑦 ) ↔ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
121	115 120	bitrd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
122	121	biimpd	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 → ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
123	122	impr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑝 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ) ) → ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
124		bdayelon	⊢ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ On
125		naddcl	⊢ ( ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ On ∧ ( bday ‘ 𝑦 ) ∈ On ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ On )
126	124 27 125	mp2an	⊢ ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ On
127	126	onordi	⊢ Ord ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) )
128		ordtr2	⊢ ( ( Ord ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∧ Ord ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∧ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
129	127 70 128	mp2an	⊢ ( ( ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∧ ( bday ‘ ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) +s 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
130	108 123 129	syl2anc	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ ( 𝑝 ∈ On ∧ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ) ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
131	130	expr	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
132		onslt	⊢ ( ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ∈ Ons ∧ 𝑥 ∈ Ons ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ ( bday ‘ 𝑥 ) ) )
133	105 132	sylan	⊢ ( ( 𝑝 ∈ On ∧ 𝑥 ∈ Ons ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ ( bday ‘ 𝑥 ) ) )
134	133	ancoms	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ ( bday ‘ 𝑥 ) ) )
135	105	fvresd	⊢ ( 𝑝 ∈ On → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) = ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) )
136		f1ocnvfv2	⊢ ( ( ( bday ↾ Ons ) : Ons –1-1-onto→ On ∧ 𝑝 ∈ On ) → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) = 𝑝 )
137	41 136	mpan	⊢ ( 𝑝 ∈ On → ( ( bday ↾ Ons ) ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) = 𝑝 )
138	135 137	eqtr3d	⊢ ( 𝑝 ∈ On → ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) = 𝑝 )
139	138	eleq1d	⊢ ( 𝑝 ∈ On → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ ( bday ‘ 𝑥 ) ↔ 𝑝 ∈ ( bday ‘ 𝑥 ) ) )
140	139	adantl	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑝 ∈ On ) → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) ∈ ( bday ‘ 𝑥 ) ↔ 𝑝 ∈ ( bday ‘ 𝑥 ) ) )
141	134 140	bitrd	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ 𝑝 ∈ ( bday ‘ 𝑥 ) ) )
142	141	ad4ant14	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) <s 𝑥 ↔ 𝑝 ∈ ( bday ‘ 𝑥 ) ) )
143	138	oveq1d	⊢ ( 𝑝 ∈ On → ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) = ( 𝑝 +no ( bday ‘ 𝑦 ) ) )
144	143	eleq1d	⊢ ( 𝑝 ∈ On → ( ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
145	144	adantl	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( ( ( bday ‘ ( ◡ ( bday ↾ Ons ) ‘ 𝑝 ) ) +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ↔ ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
146	131 142 145	3imtr3d	⊢ ( ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) ∧ 𝑝 ∈ On ) → ( 𝑝 ∈ ( bday ‘ 𝑥 ) → ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
147	146	ex	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑝 ∈ On → ( 𝑝 ∈ ( bday ‘ 𝑥 ) → ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
148	96 147	syl5	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑝 ∈ ( bday ‘ 𝑥 ) → ( 𝑝 ∈ ( bday ‘ 𝑥 ) → ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
149	148	pm2.43d	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( 𝑝 ∈ ( bday ‘ 𝑥 ) → ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
150	149	ralrimiv	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
151		eleq2	⊢ ( 𝑎 = ( bday ‘ ( 𝑥 +s 𝑦 ) ) → ( ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ↔ ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
152	151	ralbidv	⊢ ( 𝑎 = ( bday ‘ ( 𝑥 +s 𝑦 ) ) → ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ↔ ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
153		eleq2	⊢ ( 𝑎 = ( bday ‘ ( 𝑥 +s 𝑦 ) ) → ( ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ↔ ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
154	153	ralbidv	⊢ ( 𝑎 = ( bday ‘ ( 𝑥 +s 𝑦 ) ) → ( ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ↔ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
155	152 154	anbi12d	⊢ ( 𝑎 = ( bday ‘ ( 𝑥 +s 𝑦 ) ) → ( ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) ↔ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
156	155	elrab3	⊢ ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ On → ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } ↔ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) ) )
157	69 156	ax-mp	⊢ ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } ↔ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
158	95 150 157	sylanbrc	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } )
159		intss1	⊢ ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ∈ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } → ∩ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
160	158 159	syl	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ∩ { 𝑎 ∈ On ∣ ( ∀ 𝑞 ∈ ( bday ‘ 𝑦 ) ( ( bday ‘ 𝑥 ) +no 𝑞 ) ∈ 𝑎 ∧ ∀ 𝑝 ∈ ( bday ‘ 𝑥 ) ( 𝑝 +no ( bday ‘ 𝑦 ) ) ∈ 𝑎 ) } ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
161	29 160	eqsstrid	⊢ ( ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) ∧ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) )
162	161	ex	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ⊆ ( bday ‘ ( 𝑥 +s 𝑦 ) ) ) )
163	8 13 16 20 25 162	ons2ind	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ⊆ ( bday ‘ ( 𝐴 +s 𝐵 ) ) )
164	4 163	eqssd	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )