Metamath Proof Explorer

Theorem addbday

Description: The birthday of the sum of two surreals is less than or equal to the natural ordinal sum of their individual birthdays. Theorem 6.1 of Gonshor p. 95. (Contributed by Scott Fenton, 12-Aug-2025)

Ref Expression
Assertion addbday ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) )
2 fveq2 ⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑥𝑂 ) )
3 2 oveq1d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) )
4 1 3 sseq12d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ) )
5 oveq2 ⊢ ( 𝑦 = 𝑦𝑂 → ( 𝑥𝑂 +s 𝑦 ) = ( 𝑥𝑂 +s 𝑦𝑂 ) )
6 5 fveq2d ⊢ ( 𝑦 = 𝑦𝑂 → ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) )
7 fveq2 ⊢ ( 𝑦 = 𝑦𝑂 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑦𝑂 ) )
8 7 oveq2d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) )
9 6 8 sseq12d ⊢ ( 𝑦 = 𝑦𝑂 → ( ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ) )
10 fvoveq1 ⊢ ( 𝑥 = 𝑥𝑂 → ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) )
11 2 oveq1d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) )
12 10 11 sseq12d ⊢ ( 𝑥 = 𝑥𝑂 → ( ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ↔ ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ) )
13 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( 𝐴 +s 𝑦 ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝐴 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝐴 ) )
15 14 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) )
16 13 15 sseq12d ⊢ ( 𝑥 = 𝐴 → ( ( bday ‘ ( 𝑥 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ ( 𝐴 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ) )
17 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 +s 𝑦 ) = ( 𝐴 +s 𝐵 ) )
18 17 fveq2d ⊢ ( 𝑦 = 𝐵 → ( bday ‘ ( 𝐴 +s 𝑦 ) ) = ( bday ‘ ( 𝐴 +s 𝐵 ) ) )
19 fveq2 ⊢ ( 𝑦 = 𝐵 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝐵 ) )
20 19 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
21 18 20 sseq12d ⊢ ( 𝑦 = 𝐵 → ( ( bday ‘ ( 𝐴 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦 ) ) ↔ ( bday ‘ ( 𝐴 +s 𝐵 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
22 addsval2 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( 𝑥 +s 𝑦 ) = ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) )
23 22 fveq2d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) )
24 23 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday ‘ ( 𝑥 +s 𝑦 ) ) = ( bday ‘ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) )
25 simpl ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → 𝑥 ∈ No )
26 simpr ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → 𝑦 ∈ No )
27 25 26 addcuts2 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) <<s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) )
28 imaundi ⊢ ( bday “ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∪ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) = ( ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ∪ ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) )
29 imaundi ⊢ ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) = ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) )
30 imaundi ⊢ ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) = ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) )
31 29 30 uneq12i ⊢ ( ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ∪ ( bday “ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) = ( ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ∪ ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) )
32 28 31 eqtri ⊢ ( bday “ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∪ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) = ( ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ∪ ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) )
33 simplr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → 𝑦 ∈ No )
34 simpr2 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) )
35 simplr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → 𝑦 ∈ No )
36 leftssno ⊢ ( L ‘ 𝑥 ) ⊆ No
37 rightssno ⊢ ( R ‘ 𝑥 ) ⊆ No
38 36 37 unssi ⊢ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ⊆ No
39 38 sseli ⊢ ( 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) → 𝑥𝑂 ∈ No )
40 39 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → 𝑥𝑂 ∈ No )
41 35 40 addscomd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑦 +s 𝑥𝑂 ) = ( 𝑥𝑂 +s 𝑦 ) )
42 41 fveq2d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( bday ‘ ( 𝑦 +s 𝑥𝑂 ) ) = ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) )
43 bdayon ⊢ ( bday ‘ 𝑦 ) ∈ On
44 bdayon ⊢ ( bday ‘ 𝑥𝑂 ) ∈ On
45 naddcom ⊢ ( ( ( bday ‘ 𝑦 ) ∈ On ∧ ( bday ‘ 𝑥𝑂 ) ∈ On ) → ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) )
46 43 44 45 mp2an ⊢ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) )
47 46 a1i ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) = ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) )
48 42 47 sseq12d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ( bday ‘ ( 𝑦 +s 𝑥𝑂 ) ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) ↔ ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ) )
49 48 ralbidva ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑦 +s 𝑥𝑂 ) ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) ↔ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ) )
50 49 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑦 +s 𝑥𝑂 ) ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) ↔ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ) )
51 34 50 mpbird ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑦 +s 𝑥𝑂 ) ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥𝑂 ) ) )
52 ssun1 ⊢ ( L ‘ 𝑥 ) ⊆ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) )
53 33 51 52 addbdaylem ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝐿 ) } ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥 ) ) )
54 36 sseli ⊢ ( 𝑥𝐿 ∈ ( L ‘ 𝑥 ) → 𝑥𝐿 ∈ No )
55 54 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑥𝐿 ∈ No )
56 simplr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → 𝑦 ∈ No )
57 55 56 addscomd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑥𝐿 +s 𝑦 ) = ( 𝑦 +s 𝑥𝐿 ) )
58 57 eqeq2d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) ) → ( 𝑧 = ( 𝑥𝐿 +s 𝑦 ) ↔ 𝑧 = ( 𝑦 +s 𝑥𝐿 ) ) )
59 58 rexbidva ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) ↔ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝐿 ) ) )
60 59 abbidv ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝐿 ) } )
61 60 imaeq2d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) = ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝐿 ) } ) )
62 61 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) = ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝐿 ) } ) )
63 bdayon ⊢ ( bday ‘ 𝑥 ) ∈ On
64 naddcom ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝑦 ) ∈ On ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥 ) ) )
65 63 43 64 mp2an ⊢ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥 ) )
66 65 a1i ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥 ) ) )
67 53 62 66 3sstr4d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
68 simpll ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → 𝑥 ∈ No )
69 simpr3 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) )
70 ssun1 ⊢ ( L ‘ 𝑦 ) ⊆ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
71 68 69 70 addbdaylem ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
72 67 71 unssd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
73 ssun2 ⊢ ( R ‘ 𝑥 ) ⊆ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) )
74 33 51 73 addbdaylem ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝑅 ) } ) ⊆ ( ( bday ‘ 𝑦 ) +no ( bday ‘ 𝑥 ) ) )
75 37 sseli ⊢ ( 𝑥𝑅 ∈ ( R ‘ 𝑥 ) → 𝑥𝑅 ∈ No )
76 75 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑥𝑅 ∈ No )
77 simplr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → 𝑦 ∈ No )
78 76 77 addscomd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑥𝑅 +s 𝑦 ) = ( 𝑦 +s 𝑥𝑅 ) )
79 78 eqeq2d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) ) → ( 𝑧 = ( 𝑥𝑅 +s 𝑦 ) ↔ 𝑧 = ( 𝑦 +s 𝑥𝑅 ) ) )
80 79 rexbidva ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝑅 ) ) )
81 80 abbidv ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } = { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝑅 ) } )
82 81 imaeq2d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) = ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝑅 ) } ) )
83 82 adantr ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) = ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑦 +s 𝑥𝑅 ) } ) )
84 74 83 66 3sstr4d ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
85 ssun2 ⊢ ( R ‘ 𝑦 ) ⊆ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
86 68 69 85 addbdaylem ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
87 84 86 unssd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
88 72 87 unssd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ∪ ( ( bday “ { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ) ∪ ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
89 32 88 eqsstrid ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday “ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∪ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
90 naddcl ⊢ ( ( ( bday ‘ 𝑥 ) ∈ On ∧ ( bday ‘ 𝑦 ) ∈ On ) → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∈ On )
91 63 43 90 mp2an ⊢ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∈ On
92 cutbdaybnd ⊢ ( ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) <<s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∧ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∈ On ∧ ( bday “ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∪ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ) → ( bday ‘ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
93 91 92 mp3an2 ⊢ ( ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) <<s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∧ ( bday “ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ∪ ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ) → ( bday ‘ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
94 27 89 93 syl2an2r ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday ‘ ( ( { 𝑧 ∣ ∃ 𝑥𝐿 ∈ ( L ‘ 𝑥 ) 𝑧 = ( 𝑥𝐿 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( L ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) |s ( { 𝑧 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝑥 ) 𝑧 = ( 𝑥𝑅 +s 𝑦 ) } ∪ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ ( R ‘ 𝑦 ) 𝑧 = ( 𝑥 +s 𝑦𝐿 ) } ) ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
95 24 94 eqsstrd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) ) → ( bday ‘ ( 𝑥 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) )
96 95 ex ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ( ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦𝑂 ) ) ∧ ∀ 𝑥𝑂 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( bday ‘ ( 𝑥𝑂 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥𝑂 ) +no ( bday ‘ 𝑦 ) ) ∧ ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( bday ‘ ( 𝑥 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦𝑂 ) ) ) → ( bday ‘ ( 𝑥 +s 𝑦 ) ) ⊆ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ) )
97 4 9 12 16 21 96 no2inds ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ) → ( bday ‘ ( 𝐴 +s 𝐵 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )