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

Theorem addsprop 27291
Description: Inductively show that surreal addition is closed and compatible with less-than. This proof follows from induction on the birthdays of the surreal numbers involved. This pattern occurs throughout surreal development. Theorem 3.1 of [Gonshor] p. 14. (Contributed by Scott Fenton, 21-Jan-2025.)
Assertion
Ref Expression
addsprop ((𝑋 No 𝑌 No 𝑍 No ) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))

Proof of Theorem addsprop
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑝 𝑞 𝑟 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bdayelon 27119 . . . . 5 ( bday 𝑋) ∈ On
2 bdayelon 27119 . . . . 5 ( bday 𝑌) ∈ On
3 naddcl 8624 . . . . 5 ((( bday 𝑋) ∈ On ∧ ( bday 𝑌) ∈ On) → (( bday 𝑋) +no ( bday 𝑌)) ∈ On)
41, 2, 3mp2an 691 . . . 4 (( bday 𝑋) +no ( bday 𝑌)) ∈ On
5 bdayelon 27119 . . . . 5 ( bday 𝑍) ∈ On
6 naddcl 8624 . . . . 5 ((( bday 𝑋) ∈ On ∧ ( bday 𝑍) ∈ On) → (( bday 𝑋) +no ( bday 𝑍)) ∈ On)
71, 5, 6mp2an 691 . . . 4 (( bday 𝑋) +no ( bday 𝑍)) ∈ On
84, 7onun2i 6440 . . 3 ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) ∈ On
9 risset 3222 . . 3 (((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) ∈ On ↔ ∃𝑎 ∈ On 𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
108, 9mpbi 229 . 2 𝑎 ∈ On 𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍)))
11 eqeq1 2741 . . . . . . . . . 10 (𝑎 = 𝑏 → (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ↔ 𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧)))))
1211imbi1d 342 . . . . . . . . 9 (𝑎 = 𝑏 → ((𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))))
1312ralbidv 3175 . . . . . . . 8 (𝑎 = 𝑏 → (∀𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑧 No (𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))))
14132ralbidv 3213 . . . . . . 7 (𝑎 = 𝑏 → (∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑥 No 𝑦 No 𝑧 No (𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))))
15 fveq2 6843 . . . . . . . . . . . 12 (𝑥 = 𝑝 → ( bday 𝑥) = ( bday 𝑝))
1615oveq1d 7373 . . . . . . . . . . 11 (𝑥 = 𝑝 → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝑝) +no ( bday 𝑦)))
1715oveq1d 7373 . . . . . . . . . . 11 (𝑥 = 𝑝 → (( bday 𝑥) +no ( bday 𝑧)) = (( bday 𝑝) +no ( bday 𝑧)))
1816, 17uneq12d 4125 . . . . . . . . . 10 (𝑥 = 𝑝 → ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) = ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧))))
1918eqeq2d 2748 . . . . . . . . 9 (𝑥 = 𝑝 → (𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ↔ 𝑏 = ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧)))))
20 oveq1 7365 . . . . . . . . . . 11 (𝑥 = 𝑝 → (𝑥 +s 𝑦) = (𝑝 +s 𝑦))
2120eleq1d 2823 . . . . . . . . . 10 (𝑥 = 𝑝 → ((𝑥 +s 𝑦) ∈ No ↔ (𝑝 +s 𝑦) ∈ No ))
22 oveq2 7366 . . . . . . . . . . . 12 (𝑥 = 𝑝 → (𝑦 +s 𝑥) = (𝑦 +s 𝑝))
23 oveq2 7366 . . . . . . . . . . . 12 (𝑥 = 𝑝 → (𝑧 +s 𝑥) = (𝑧 +s 𝑝))
2422, 23breq12d 5119 . . . . . . . . . . 11 (𝑥 = 𝑝 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))
2524imbi2d 341 . . . . . . . . . 10 (𝑥 = 𝑝 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))))
2621, 25anbi12d 632 . . . . . . . . 9 (𝑥 = 𝑝 → (((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝑝 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))))
2719, 26imbi12d 345 . . . . . . . 8 (𝑥 = 𝑝 → ((𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑏 = ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧))) → ((𝑝 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))))))
28 fveq2 6843 . . . . . . . . . . . 12 (𝑦 = 𝑞 → ( bday 𝑦) = ( bday 𝑞))
2928oveq2d 7374 . . . . . . . . . . 11 (𝑦 = 𝑞 → (( bday 𝑝) +no ( bday 𝑦)) = (( bday 𝑝) +no ( bday 𝑞)))
3029uneq1d 4123 . . . . . . . . . 10 (𝑦 = 𝑞 → ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧))) = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧))))
3130eqeq2d 2748 . . . . . . . . 9 (𝑦 = 𝑞 → (𝑏 = ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧))) ↔ 𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧)))))
32 oveq2 7366 . . . . . . . . . . 11 (𝑦 = 𝑞 → (𝑝 +s 𝑦) = (𝑝 +s 𝑞))
3332eleq1d 2823 . . . . . . . . . 10 (𝑦 = 𝑞 → ((𝑝 +s 𝑦) ∈ No ↔ (𝑝 +s 𝑞) ∈ No ))
34 breq1 5109 . . . . . . . . . . 11 (𝑦 = 𝑞 → (𝑦 <s 𝑧𝑞 <s 𝑧))
35 oveq1 7365 . . . . . . . . . . . 12 (𝑦 = 𝑞 → (𝑦 +s 𝑝) = (𝑞 +s 𝑝))
3635breq1d 5116 . . . . . . . . . . 11 (𝑦 = 𝑞 → ((𝑦 +s 𝑝) <s (𝑧 +s 𝑝) ↔ (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))
3734, 36imbi12d 345 . . . . . . . . . 10 (𝑦 = 𝑞 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)) ↔ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))))
3833, 37anbi12d 632 . . . . . . . . 9 (𝑦 = 𝑞 → (((𝑝 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))) ↔ ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))))
3931, 38imbi12d 345 . . . . . . . 8 (𝑦 = 𝑞 → ((𝑏 = ((( bday 𝑝) +no ( bday 𝑦)) ∪ (( bday 𝑝) +no ( bday 𝑧))) → ((𝑝 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))) ↔ (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))))))
40 fveq2 6843 . . . . . . . . . . . 12 (𝑧 = 𝑟 → ( bday 𝑧) = ( bday 𝑟))
4140oveq2d 7374 . . . . . . . . . . 11 (𝑧 = 𝑟 → (( bday 𝑝) +no ( bday 𝑧)) = (( bday 𝑝) +no ( bday 𝑟)))
4241uneq2d 4124 . . . . . . . . . 10 (𝑧 = 𝑟 → ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧))) = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))))
4342eqeq2d 2748 . . . . . . . . 9 (𝑧 = 𝑟 → (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧))) ↔ 𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟)))))
44 breq2 5110 . . . . . . . . . . 11 (𝑧 = 𝑟 → (𝑞 <s 𝑧𝑞 <s 𝑟))
45 oveq1 7365 . . . . . . . . . . . 12 (𝑧 = 𝑟 → (𝑧 +s 𝑝) = (𝑟 +s 𝑝))
4645breq2d 5118 . . . . . . . . . . 11 (𝑧 = 𝑟 → ((𝑞 +s 𝑝) <s (𝑧 +s 𝑝) ↔ (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))
4744, 46imbi12d 345 . . . . . . . . . 10 (𝑧 = 𝑟 → ((𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)) ↔ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))
4847anbi2d 630 . . . . . . . . 9 (𝑧 = 𝑟 → (((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))) ↔ ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
4943, 48imbi12d 345 . . . . . . . 8 (𝑧 = 𝑟 → ((𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))) ↔ (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))))
5027, 39, 49cbvral3vw 3230 . . . . . . 7 (∀𝑥 No 𝑦 No 𝑧 No (𝑏 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
5114, 50bitrdi 287 . . . . . 6 (𝑎 = 𝑏 → (∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))))
52 ralrot3 3277 . . . . . . . . 9 (∀𝑝 No 𝑞 No 𝑏𝑎𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑏𝑎𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
53 ralcom 3273 . . . . . . . . . . 11 (∀𝑏𝑎𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 No 𝑏𝑎 (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
54 r19.23v 3180 . . . . . . . . . . . . 13 (∀𝑏𝑎 (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (∃𝑏𝑎 𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
55 risset 3222 . . . . . . . . . . . . . 14 (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 ↔ ∃𝑏𝑎 𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))))
5655imbi1i 350 . . . . . . . . . . . . 13 ((((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (∃𝑏𝑎 𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
5754, 56bitr4i 278 . . . . . . . . . . . 12 (∀𝑏𝑎 (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
5857ralbii 3097 . . . . . . . . . . 11 (∀𝑟 No 𝑏𝑎 (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
5953, 58bitri 275 . . . . . . . . . 10 (∀𝑏𝑎𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
60592ralbii 3128 . . . . . . . . 9 (∀𝑝 No 𝑞 No 𝑏𝑎𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
6152, 60bitr3i 277 . . . . . . . 8 (∀𝑏𝑎𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
62 eleq2 2827 . . . . . . . . . . . . . . . . 17 (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 ↔ ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧)))))
6362imbi1d 342 . . . . . . . . . . . . . . . 16 (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))))
6463ralbidv 3175 . . . . . . . . . . . . . . 15 (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → (∀𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))))
65642ralbidv 3213 . . . . . . . . . . . . . 14 (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → (∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))))
6665anbi1d 631 . . . . . . . . . . . . 13 (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ↔ (∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No ))))
6766biimpcd 249 . . . . . . . . . . . 12 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → (∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No ))))
68 simpl 484 . . . . . . . . . . . . . . 15 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → ∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
69 simprll 778 . . . . . . . . . . . . . . 15 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → 𝑥 No )
70 simprlr 779 . . . . . . . . . . . . . . 15 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → 𝑦 No )
7168, 69, 70addsproplem3 27286 . . . . . . . . . . . . . 14 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → ((𝑥 +s 𝑦) ∈ No ∧ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑥)𝑎 = (𝑏 +s 𝑦)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑦)𝑐 = (𝑥 +s 𝑑)}) <<s {(𝑥 +s 𝑦)} ∧ {(𝑥 +s 𝑦)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑥)𝑒 = (𝑓 +s 𝑦)} ∪ {𝑔 ∣ ∃ ∈ ( R ‘𝑦)𝑔 = (𝑥 +s )})))
7271simp1d 1143 . . . . . . . . . . . . 13 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → (𝑥 +s 𝑦) ∈ No )
7368adantr 482 . . . . . . . . . . . . . . 15 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → ∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))
7469adantr 482 . . . . . . . . . . . . . . 15 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → 𝑥 No )
7570adantr 482 . . . . . . . . . . . . . . 15 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → 𝑦 No )
76 simplrr 777 . . . . . . . . . . . . . . 15 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → 𝑧 No )
77 simpr 486 . . . . . . . . . . . . . . 15 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → 𝑦 <s 𝑧)
7873, 74, 75, 76, 77addsproplem7 27290 . . . . . . . . . . . . . 14 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) ∧ 𝑦 <s 𝑧) → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))
7978ex 414 . . . . . . . . . . . . 13 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))
8072, 79jca 513 . . . . . . . . . . . 12 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))
8167, 80syl6 35 . . . . . . . . . . 11 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 No 𝑦 No ) ∧ 𝑧 No )) → (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
8281anassrs 469 . . . . . . . . . 10 (((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ (𝑥 No 𝑦 No )) ∧ 𝑧 No ) → (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
8382ralrimiva 3144 . . . . . . . . 9 ((∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ (𝑥 No 𝑦 No )) → ∀𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
8483ralrimivva 3198 . . . . . . . 8 (∀𝑝 No 𝑞 No 𝑟 No (((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
8561, 84sylbi 216 . . . . . . 7 (∀𝑏𝑎𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
8685a1i 11 . . . . . 6 (𝑎 ∈ On → (∀𝑏𝑎𝑝 No 𝑞 No 𝑟 No (𝑏 = ((( bday 𝑝) +no ( bday 𝑞)) ∪ (( bday 𝑝) +no ( bday 𝑟))) → ((𝑝 +s 𝑞) ∈ No ∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))))
8751, 86tfis2 7794 . . . . 5 (𝑎 ∈ On → ∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))
88 fveq2 6843 . . . . . . . . . 10 (𝑥 = 𝑋 → ( bday 𝑥) = ( bday 𝑋))
8988oveq1d 7373 . . . . . . . . 9 (𝑥 = 𝑋 → (( bday 𝑥) +no ( bday 𝑦)) = (( bday 𝑋) +no ( bday 𝑦)))
9088oveq1d 7373 . . . . . . . . 9 (𝑥 = 𝑋 → (( bday 𝑥) +no ( bday 𝑧)) = (( bday 𝑋) +no ( bday 𝑧)))
9189, 90uneq12d 4125 . . . . . . . 8 (𝑥 = 𝑋 → ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) = ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧))))
9291eqeq2d 2748 . . . . . . 7 (𝑥 = 𝑋 → (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) ↔ 𝑎 = ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧)))))
93 oveq1 7365 . . . . . . . . 9 (𝑥 = 𝑋 → (𝑥 +s 𝑦) = (𝑋 +s 𝑦))
9493eleq1d 2823 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑥 +s 𝑦) ∈ No ↔ (𝑋 +s 𝑦) ∈ No ))
95 oveq2 7366 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑦 +s 𝑥) = (𝑦 +s 𝑋))
96 oveq2 7366 . . . . . . . . . 10 (𝑥 = 𝑋 → (𝑧 +s 𝑥) = (𝑧 +s 𝑋))
9795, 96breq12d 5119 . . . . . . . . 9 (𝑥 = 𝑋 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))
9897imbi2d 341 . . . . . . . 8 (𝑥 = 𝑋 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))))
9994, 98anbi12d 632 . . . . . . 7 (𝑥 = 𝑋 → (((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝑋 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))))
10092, 99imbi12d 345 . . . . . 6 (𝑥 = 𝑋 → ((𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑎 = ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧))) → ((𝑋 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))))))
101 fveq2 6843 . . . . . . . . . 10 (𝑦 = 𝑌 → ( bday 𝑦) = ( bday 𝑌))
102101oveq2d 7374 . . . . . . . . 9 (𝑦 = 𝑌 → (( bday 𝑋) +no ( bday 𝑦)) = (( bday 𝑋) +no ( bday 𝑌)))
103102uneq1d 4123 . . . . . . . 8 (𝑦 = 𝑌 → ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧))) = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧))))
104103eqeq2d 2748 . . . . . . 7 (𝑦 = 𝑌 → (𝑎 = ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧))) ↔ 𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧)))))
105 oveq2 7366 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑋 +s 𝑦) = (𝑋 +s 𝑌))
106105eleq1d 2823 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑋 +s 𝑦) ∈ No ↔ (𝑋 +s 𝑌) ∈ No ))
107 breq1 5109 . . . . . . . . 9 (𝑦 = 𝑌 → (𝑦 <s 𝑧𝑌 <s 𝑧))
108 oveq1 7365 . . . . . . . . . 10 (𝑦 = 𝑌 → (𝑦 +s 𝑋) = (𝑌 +s 𝑋))
109108breq1d 5116 . . . . . . . . 9 (𝑦 = 𝑌 → ((𝑦 +s 𝑋) <s (𝑧 +s 𝑋) ↔ (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))
110107, 109imbi12d 345 . . . . . . . 8 (𝑦 = 𝑌 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)) ↔ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))))
111106, 110anbi12d 632 . . . . . . 7 (𝑦 = 𝑌 → (((𝑋 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))) ↔ ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))))
112104, 111imbi12d 345 . . . . . 6 (𝑦 = 𝑌 → ((𝑎 = ((( bday 𝑋) +no ( bday 𝑦)) ∪ (( bday 𝑋) +no ( bday 𝑧))) → ((𝑋 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))) ↔ (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧))) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))))))
113 fveq2 6843 . . . . . . . . . 10 (𝑧 = 𝑍 → ( bday 𝑧) = ( bday 𝑍))
114113oveq2d 7374 . . . . . . . . 9 (𝑧 = 𝑍 → (( bday 𝑋) +no ( bday 𝑧)) = (( bday 𝑋) +no ( bday 𝑍)))
115114uneq2d 4124 . . . . . . . 8 (𝑧 = 𝑍 → ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧))) = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))))
116115eqeq2d 2748 . . . . . . 7 (𝑧 = 𝑍 → (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧))) ↔ 𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍)))))
117 breq2 5110 . . . . . . . . 9 (𝑧 = 𝑍 → (𝑌 <s 𝑧𝑌 <s 𝑍))
118 oveq1 7365 . . . . . . . . . 10 (𝑧 = 𝑍 → (𝑧 +s 𝑋) = (𝑍 +s 𝑋))
119118breq2d 5118 . . . . . . . . 9 (𝑧 = 𝑍 → ((𝑌 +s 𝑋) <s (𝑧 +s 𝑋) ↔ (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))
120117, 119imbi12d 345 . . . . . . . 8 (𝑧 = 𝑍 → ((𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)) ↔ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))
121120anbi2d 630 . . . . . . 7 (𝑧 = 𝑍 → (((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))) ↔ ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))
122116, 121imbi12d 345 . . . . . 6 (𝑧 = 𝑍 → ((𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑧))) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))) ↔ (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))))
123100, 112, 122rspc3v 3594 . . . . 5 ((𝑋 No 𝑌 No 𝑍 No ) → (∀𝑥 No 𝑦 No 𝑧 No (𝑎 = ((( bday 𝑥) +no ( bday 𝑦)) ∪ (( bday 𝑥) +no ( bday 𝑧))) → ((𝑥 +s 𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) → (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))))
12487, 123syl5com 31 . . . 4 (𝑎 ∈ On → ((𝑋 No 𝑌 No 𝑍 No ) → (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))))
125124com23 86 . . 3 (𝑎 ∈ On → (𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑋 No 𝑌 No 𝑍 No ) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))))
126125rexlimiv 3146 . 2 (∃𝑎 ∈ On 𝑎 = ((( bday 𝑋) +no ( bday 𝑌)) ∪ (( bday 𝑋) +no ( bday 𝑍))) → ((𝑋 No 𝑌 No 𝑍 No ) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))
12710, 126ax-mp 5 1 ((𝑋 No 𝑌 No 𝑍 No ) → ((𝑋 +s 𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088   = wceq 1542  wcel 2107  {cab 2714  wral 3065  wrex 3074  cun 3909  {csn 4587   class class class wbr 5106  Oncon0 6318  cfv 6497  (class class class)co 7358   +no cnadd 8612   No csur 26991   <s cslt 26992   bday cbday 26993   <<s csslt 27123   L cleft 27178   R cright 27179   +s cadds 27274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-tp 4592  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-1o 8413  df-2o 8414  df-nadd 8613  df-no 26994  df-slt 26995  df-bday 26996  df-sslt 27124  df-scut 27126  df-0s 27166  df-made 27180  df-old 27181  df-left 27183  df-right 27184  df-norec2 27264  df-adds 27275
This theorem is referenced by:  addscut  27292  sltadd1im  27297
  Copyright terms: Public domain W3C validator