MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addsbday Structured version   Visualization version   GIF version

Theorem addsbday 28068
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.)
Assertion
Ref Expression
addsbday ((𝐴 No 𝐵 No ) → ( bday ‘(𝐴 +s 𝐵)) ⊆ (( bday 𝐴) +no ( bday 𝐵)))

Proof of Theorem addsbday
Dummy variables 𝑥 𝑦 𝑥𝑂 𝑦𝑂 𝑥𝐿 𝑦𝐿 𝑥𝑅 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fvoveq1 7471 . . 3 (𝑥 = 𝑥𝑂 → ( bday ‘(𝑥 +s 𝑦)) = ( bday ‘(𝑥𝑂 +s 𝑦)))
2 fveq2 6920 . . . 4 (𝑥 = 𝑥𝑂 → ( bday 𝑥) = ( bday 𝑥𝑂))
32oveq1d 7463 . . 3 (𝑥 = 𝑥𝑂 → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝑥𝑂) +no ( bday 𝑦)))
41, 3sseq12d 4042 . 2 (𝑥 = 𝑥𝑂 → (( bday ‘(𝑥 +s 𝑦)) ⊆ (( bday 𝑥) +no ( bday 𝑦)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦))))
5 oveq2 7456 . . . 4 (𝑦 = 𝑦𝑂 → (𝑥𝑂 +s 𝑦) = (𝑥𝑂 +s 𝑦𝑂))
65fveq2d 6924 . . 3 (𝑦 = 𝑦𝑂 → ( bday ‘(𝑥𝑂 +s 𝑦)) = ( bday ‘(𝑥𝑂 +s 𝑦𝑂)))
7 fveq2 6920 . . . 4 (𝑦 = 𝑦𝑂 → ( bday 𝑦) = ( bday 𝑦𝑂))
87oveq2d 7464 . . 3 (𝑦 = 𝑦𝑂 → (( bday 𝑥𝑂) +no ( bday 𝑦)) = (( bday 𝑥𝑂) +no ( bday 𝑦𝑂)))
96, 8sseq12d 4042 . 2 (𝑦 = 𝑦𝑂 → (( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦𝑂)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦𝑂))))
10 fvoveq1 7471 . . 3 (𝑥 = 𝑥𝑂 → ( bday ‘(𝑥 +s 𝑦𝑂)) = ( bday ‘(𝑥𝑂 +s 𝑦𝑂)))
112oveq1d 7463 . . 3 (𝑥 = 𝑥𝑂 → (( bday 𝑥) +no ( bday 𝑦𝑂)) = (( bday 𝑥𝑂) +no ( bday 𝑦𝑂)))
1210, 11sseq12d 4042 . 2 (𝑥 = 𝑥𝑂 → (( bday ‘(𝑥 +s 𝑦𝑂)) ⊆ (( bday 𝑥) +no ( bday 𝑦𝑂)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦𝑂)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦𝑂))))
13 fvoveq1 7471 . . 3 (𝑥 = 𝐴 → ( bday ‘(𝑥 +s 𝑦)) = ( bday ‘(𝐴 +s 𝑦)))
14 fveq2 6920 . . . 4 (𝑥 = 𝐴 → ( bday 𝑥) = ( bday 𝐴))
1514oveq1d 7463 . . 3 (𝑥 = 𝐴 → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝐴) +no ( bday 𝑦)))
1613, 15sseq12d 4042 . 2 (𝑥 = 𝐴 → (( bday ‘(𝑥 +s 𝑦)) ⊆ (( bday 𝑥) +no ( bday 𝑦)) ↔ ( bday ‘(𝐴 +s 𝑦)) ⊆ (( bday 𝐴) +no ( bday 𝑦))))
17 oveq2 7456 . . . 4 (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵))
1817fveq2d 6924 . . 3 (𝑦 = 𝐵 → ( bday ‘(𝐴 +s 𝑦)) = ( bday ‘(𝐴 +s 𝐵)))
19 fveq2 6920 . . . 4 (𝑦 = 𝐵 → ( bday 𝑦) = ( bday 𝐵))
2019oveq2d 7464 . . 3 (𝑦 = 𝐵 → (( bday 𝐴) +no ( bday 𝑦)) = (( bday 𝐴) +no ( bday 𝐵)))
2118, 20sseq12d 4042 . 2 (𝑦 = 𝐵 → (( bday ‘(𝐴 +s 𝑦)) ⊆ (( bday 𝐴) +no ( bday 𝑦)) ↔ ( bday ‘(𝐴 +s 𝐵)) ⊆ (( bday 𝐴) +no ( bday 𝐵))))
22 addsval2 28014 . . . . . 6 ((𝑥 No 𝑦 No ) → (𝑥 +s 𝑦) = (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))
2322fveq2d 6924 . . . . 5 ((𝑥 No 𝑦 No ) → ( bday ‘(𝑥 +s 𝑦)) = ( bday ‘(({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))))
2423adantr 480 . . . 4 (((𝑥 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 482 . . . . . 6 ((𝑥 No 𝑦 No ) → 𝑥 No )
26 simpr 484 . . . . . 6 ((𝑥 No 𝑦 No ) → 𝑦 No )
2725, 26addscut2 28030 . . . . 5 ((𝑥 No 𝑦 No ) → ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) <<s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))
28 imaundi 6181 . . . . . . 7 ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = (( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))
29 imaundi 6181 . . . . . . . 8 ( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) = (( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))
30 imaundi 6181 . . . . . . . 8 ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) = (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))
3129, 30uneq12i 4189 . . . . . . 7 (( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = ((( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))
3228, 31eqtri 2768 . . . . . 6 ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = ((( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))
33 simplr 768 . . . . . . . . . 10 (((𝑥 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 1195 . . . . . . . . . . 11 (((𝑥 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 768 . . . . . . . . . . . . . . . 16 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → 𝑦 No )
36 leftssno 27937 . . . . . . . . . . . . . . . . . . 19 ( L ‘𝑥) ⊆ No
37 rightssno 27938 . . . . . . . . . . . . . . . . . . 19 ( R ‘𝑥) ⊆ No
3836, 37unssi 4214 . . . . . . . . . . . . . . . . . 18 (( L ‘𝑥) ∪ ( R ‘𝑥)) ⊆ No
3938sseli 4004 . . . . . . . . . . . . . . . . 17 (𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥)) → 𝑥𝑂 No )
4039adantl 481 . . . . . . . . . . . . . . . 16 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → 𝑥𝑂 No )
4135, 40addscomd 28018 . . . . . . . . . . . . . . 15 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (𝑦 +s 𝑥𝑂) = (𝑥𝑂 +s 𝑦))
4241fveq2d 6924 . . . . . . . . . . . . . 14 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → ( bday ‘(𝑦 +s 𝑥𝑂)) = ( bday ‘(𝑥𝑂 +s 𝑦)))
43 bdayelon 27839 . . . . . . . . . . . . . . . 16 ( bday 𝑦) ∈ On
44 bdayelon 27839 . . . . . . . . . . . . . . . 16 ( bday 𝑥𝑂) ∈ On
45 naddcom 8738 . . . . . . . . . . . . . . . 16 ((( bday 𝑦) ∈ On ∧ ( bday 𝑥𝑂) ∈ On) → (( bday 𝑦) +no ( bday 𝑥𝑂)) = (( bday 𝑥𝑂) +no ( bday 𝑦)))
4643, 44, 45mp2an 691 . . . . . . . . . . . . . . 15 (( bday 𝑦) +no ( bday 𝑥𝑂)) = (( bday 𝑥𝑂) +no ( bday 𝑦))
4746a1i 11 . . . . . . . . . . . . . 14 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (( bday 𝑦) +no ( bday 𝑥𝑂)) = (( bday 𝑥𝑂) +no ( bday 𝑦)))
4842, 47sseq12d 4042 . . . . . . . . . . . . 13 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (( bday ‘(𝑦 +s 𝑥𝑂)) ⊆ (( bday 𝑦) +no ( bday 𝑥𝑂)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦))))
4948ralbidva 3182 . . . . . . . . . . . 12 ((𝑥 No 𝑦 No ) → (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday ‘(𝑦 +s 𝑥𝑂)) ⊆ (( bday 𝑦) +no ( bday 𝑥𝑂)) ↔ ∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday 𝑥𝑂) +no ( bday 𝑦))))
5049adantr 480 . . . . . . . . . . 11 (((𝑥 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 𝑦))))
5134, 50mpbird 257 . . . . . . . . . 10 (((𝑥 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 4201 . . . . . . . . . 10 ( L ‘𝑥) ⊆ (( L ‘𝑥) ∪ ( R ‘𝑥))
5333, 51, 52addsbdaylem 28067 . . . . . . . . 9 (((𝑥 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 𝑥)))
5436sseli 4004 . . . . . . . . . . . . . . . 16 (𝑥𝐿 ∈ ( L ‘𝑥) → 𝑥𝐿 No )
5554adantl 481 . . . . . . . . . . . . . . 15 (((𝑥 No 𝑦 No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → 𝑥𝐿 No )
56 simplr 768 . . . . . . . . . . . . . . 15 (((𝑥 No 𝑦 No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → 𝑦 No )
5755, 56addscomd 28018 . . . . . . . . . . . . . 14 (((𝑥 No 𝑦 No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → (𝑥𝐿 +s 𝑦) = (𝑦 +s 𝑥𝐿))
5857eqeq2d 2751 . . . . . . . . . . . . 13 (((𝑥 No 𝑦 No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → (𝑧 = (𝑥𝐿 +s 𝑦) ↔ 𝑧 = (𝑦 +s 𝑥𝐿)))
5958rexbidva 3183 . . . . . . . . . . . 12 ((𝑥 No 𝑦 No ) → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦) ↔ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)))
6059abbidv 2811 . . . . . . . . . . 11 ((𝑥 No 𝑦 No ) → {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} = {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)})
6160imaeq2d 6089 . . . . . . . . . 10 ((𝑥 No 𝑦 No ) → ( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) = ( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)}))
6261adantr 480 . . . . . . . . 9 (((𝑥 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 bdayelon 27839 . . . . . . . . . . 11 ( bday 𝑥) ∈ On
64 naddcom 8738 . . . . . . . . . . 11 ((( bday 𝑥) ∈ On ∧ ( bday 𝑦) ∈ On) → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝑦) +no ( bday 𝑥)))
6563, 43, 64mp2an 691 . . . . . . . . . 10 (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝑦) +no ( bday 𝑥))
6665a1i 11 . . . . . . . . 9 (((𝑥 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 𝑥)))
6753, 62, 663sstr4d 4056 . . . . . . . 8 (((𝑥 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 766 . . . . . . . . 9 (((𝑥 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 1196 . . . . . . . . 9 (((𝑥 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 4201 . . . . . . . . 9 ( L ‘𝑦) ⊆ (( L ‘𝑦) ∪ ( R ‘𝑦))
7168, 69, 70addsbdaylem 28067 . . . . . . . 8 (((𝑥 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 𝑦)))
7267, 71unssd 4215 . . . . . . 7 (((𝑥 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 4202 . . . . . . . . . 10 ( R ‘𝑥) ⊆ (( L ‘𝑥) ∪ ( R ‘𝑥))
7433, 51, 73addsbdaylem 28067 . . . . . . . . 9 (((𝑥 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 𝑥)))
7537sseli 4004 . . . . . . . . . . . . . . . 16 (𝑥𝑅 ∈ ( R ‘𝑥) → 𝑥𝑅 No )
7675adantl 481 . . . . . . . . . . . . . . 15 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → 𝑥𝑅 No )
77 simplr 768 . . . . . . . . . . . . . . 15 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → 𝑦 No )
7876, 77addscomd 28018 . . . . . . . . . . . . . 14 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → (𝑥𝑅 +s 𝑦) = (𝑦 +s 𝑥𝑅))
7978eqeq2d 2751 . . . . . . . . . . . . 13 (((𝑥 No 𝑦 No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → (𝑧 = (𝑥𝑅 +s 𝑦) ↔ 𝑧 = (𝑦 +s 𝑥𝑅)))
8079rexbidva 3183 . . . . . . . . . . . 12 ((𝑥 No 𝑦 No ) → (∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦) ↔ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)))
8180abbidv 2811 . . . . . . . . . . 11 ((𝑥 No 𝑦 No ) → {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} = {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)})
8281imaeq2d 6089 . . . . . . . . . 10 ((𝑥 No 𝑦 No ) → ( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) = ( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)}))
8382adantr 480 . . . . . . . . 9 (((𝑥 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 𝑥𝑅)}))
8474, 83, 663sstr4d 4056 . . . . . . . 8 (((𝑥 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 4202 . . . . . . . . 9 ( R ‘𝑦) ⊆ (( L ‘𝑦) ∪ ( R ‘𝑦))
8668, 69, 85addsbdaylem 28067 . . . . . . . 8 (((𝑥 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 𝑦)))
8784, 86unssd 4215 . . . . . . 7 (((𝑥 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 𝑦)))
8872, 87unssd 4215 . . . . . 6 (((𝑥 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 𝑦)))
8932, 88eqsstrid 4057 . . . . 5 (((𝑥 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 8733 . . . . . . 7 ((( bday 𝑥) ∈ On ∧ ( bday 𝑦) ∈ On) → (( bday 𝑥) +no ( bday 𝑦)) ∈ On)
9163, 43, 90mp2an 691 . . . . . 6 (( bday 𝑥) +no ( bday 𝑦)) ∈ On
92 scutbdaybnd 27878 . . . . . 6 ((({𝑧 ∣ ∃𝑥𝐿 ∈ ( 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 𝑦)))
9391, 92mp3an2 1449 . . . . 5 ((({𝑧 ∣ ∃𝑥𝐿 ∈ ( 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 𝑦)))
9427, 89, 93syl2an2r 684 . . . 4 (((𝑥 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 𝑦)))
9524, 94eqsstrd 4047 . . 3 (((𝑥 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 𝑦)))
9695ex 412 . 2 ((𝑥 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 𝑦))))
974, 9, 12, 16, 21, 96no2inds 28006 1 ((𝐴 No 𝐵 No ) → ( bday ‘(𝐴 +s 𝐵)) ⊆ (( bday 𝐴) +no ( bday 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1537  wcel 2108  {cab 2717  wral 3067  wrex 3076  cun 3974  wss 3976   class class class wbr 5166  cima 5703  Oncon0 6395  cfv 6573  (class class class)co 7448   +no cnadd 8721   No csur 27702   bday cbday 27704   <<s csslt 27843   |s cscut 27845   L cleft 27902   R cright 27903   +s cadds 28010
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-tp 4653  df-op 4655  df-uni 4932  df-int 4971  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-1o 8522  df-2o 8523  df-nadd 8722  df-no 27705  df-slt 27706  df-bday 27707  df-sslt 27844  df-scut 27846  df-0s 27887  df-made 27904  df-old 27905  df-left 27907  df-right 27908  df-norec2 28000  df-adds 28011
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator