Metamath Proof Explorer

Theorem addsprop

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)

Ref Expression
Assertion addsprop ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) )

Proof

Step Hyp Ref Expression
1 bdayon ⊢ ( bday ‘ 𝑋 ) ∈ On
2 bdayon ⊢ ( bday ‘ 𝑌 ) ∈ On
3 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
4 1 2 3 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On
5 bdayon ⊢ ( bday ‘ 𝑍 ) ∈ On
6 naddcl ⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑍 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∈ On )
7 1 5 6 mp2an ⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ∈ On
8 4 7 onun2i ⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ∈ On
9 risset ⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ∈ On ↔ ∃ 𝑎 ∈ On 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
10 8 9 mpbi ⊢ ∃ 𝑎 ∈ On 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) )
11 eqeq1 ⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑏 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ) )
12 11 imbi1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑎 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ↔ ( 𝑏 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) ) )
13 12 ralbidv ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑧 ∈ 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 𝑥 ) ) ) ) ) )
14 13 2ralbidv ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ 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 ⊢ ( 𝑥 = 𝑝 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑝 ) )
16 15 oveq1d ⊢ ( 𝑥 = 𝑝 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) )
17 15 oveq1d ⊢ ( 𝑥 = 𝑝 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) )
18 16 17 uneq12d ⊢ ( 𝑥 = 𝑝 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) )
19 18 eqeq2d ⊢ ( 𝑥 = 𝑝 → ( 𝑏 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) ) )
20 oveq1 ⊢ ( 𝑥 = 𝑝 → ( 𝑥 +s 𝑦 ) = ( 𝑝 +s 𝑦 ) )
21 20 eleq1d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑥 +s 𝑦 ) ∈ No ↔ ( 𝑝 +s 𝑦 ) ∈ No ) )
22 oveq2 ⊢ ( 𝑥 = 𝑝 → ( 𝑦 +s 𝑥 ) = ( 𝑦 +s 𝑝 ) )
23 oveq2 ⊢ ( 𝑥 = 𝑝 → ( 𝑧 +s 𝑥 ) = ( 𝑧 +s 𝑝 ) )
24 22 23 breq12d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ↔ ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) )
25 24 imbi2d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ↔ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) )
26 21 25 anbi12d ⊢ ( 𝑥 = 𝑝 → ( ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ↔ ( ( 𝑝 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) ) )
27 19 26 imbi12d ⊢ ( 𝑥 = 𝑝 → ( ( 𝑏 = ( ( ( 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 ⊢ ( 𝑦 = 𝑞 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑞 ) )
29 28 oveq2d ⊢ ( 𝑦 = 𝑞 → ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) )
30 29 uneq1d ⊢ ( 𝑦 = 𝑞 → ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) )
31 30 eqeq2d ⊢ ( 𝑦 = 𝑞 → ( 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) ) )
32 oveq2 ⊢ ( 𝑦 = 𝑞 → ( 𝑝 +s 𝑦 ) = ( 𝑝 +s 𝑞 ) )
33 32 eleq1d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑝 +s 𝑦 ) ∈ No ↔ ( 𝑝 +s 𝑞 ) ∈ No ) )
34 breq1 ⊢ ( 𝑦 = 𝑞 → ( 𝑦 <s 𝑧 ↔ 𝑞 <s 𝑧 ) )
35 oveq1 ⊢ ( 𝑦 = 𝑞 → ( 𝑦 +s 𝑝 ) = ( 𝑞 +s 𝑝 ) )
36 35 breq1d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ↔ ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) )
37 34 36 imbi12d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ↔ ( 𝑞 <s 𝑧 → ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) )
38 33 37 anbi12d ⊢ ( 𝑦 = 𝑞 → ( ( ( 𝑝 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) ↔ ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑧 → ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) ) )
39 31 38 imbi12d ⊢ ( 𝑦 = 𝑞 → ( ( 𝑏 = ( ( ( 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 ⊢ ( 𝑧 = 𝑟 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝑟 ) )
41 40 oveq2d ⊢ ( 𝑧 = 𝑟 → ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) )
42 41 uneq2d ⊢ ( 𝑧 = 𝑟 → ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) )
43 42 eqeq2d ⊢ ( 𝑧 = 𝑟 → ( 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ) )
44 breq2 ⊢ ( 𝑧 = 𝑟 → ( 𝑞 <s 𝑧 ↔ 𝑞 <s 𝑟 ) )
45 oveq1 ⊢ ( 𝑧 = 𝑟 → ( 𝑧 +s 𝑝 ) = ( 𝑟 +s 𝑝 ) )
46 45 breq2d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ↔ ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) )
47 44 46 imbi12d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑞 <s 𝑧 → ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ↔ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) )
48 47 anbi2d ⊢ ( 𝑧 = 𝑟 → ( ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑧 → ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) ↔ ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) )
49 43 48 imbi12d ⊢ ( 𝑧 = 𝑟 → ( ( 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑧 → ( 𝑞 +s 𝑝 ) <s ( 𝑧 +s 𝑝 ) ) ) ) ↔ ( 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) ) )
50 27 39 49 cbvral3vw ⊢ ( ∀ 𝑥 ∈ 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 𝑝 ) ) ) ) )
51 14 50 bitrdi ⊢ ( 𝑎 = 𝑏 → ( ∀ 𝑥 ∈ 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 ⊢ ( ∀ 𝑝 ∈ 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 ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑟 ∈ 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 ⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 = ( ( ( 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 ⊢ ( ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ∈ 𝑎 ↔ ∃ 𝑏 ∈ 𝑎 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) )
56 55 imbi1i ⊢ ( ( ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ∈ 𝑎 → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) ↔ ( ∃ 𝑏 ∈ 𝑎 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) )
57 54 56 bitr4i ⊢ ( ∀ 𝑏 ∈ 𝑎 ( 𝑏 = ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) ↔ ( ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ∈ 𝑎 → ( ( 𝑝 +s 𝑞 ) ∈ No ∧ ( 𝑞 <s 𝑟 → ( 𝑞 +s 𝑝 ) <s ( 𝑟 +s 𝑝 ) ) ) ) )
58 57 ralbii ⊢ ( ∀ 𝑟 ∈ 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 𝑝 ) ) ) ) )
59 53 58 bitri ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑟 ∈ 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 𝑝 ) ) ) ) )
60 59 2ralbii ⊢ ( ∀ 𝑝 ∈ 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 𝑝 ) ) ) ) )
61 52 60 bitr3i ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑝 ∈ 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 ⊢ ( 𝑎 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ∈ 𝑎 ↔ ( ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑞 ) ) ∪ ( ( bday ‘ 𝑝 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ) )
63 62 imbi1d ⊢ ( 𝑎 = ( ( ( 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 𝑝 ) ) ) ) ) )
64 63 ralbidv ⊢ ( 𝑎 = ( ( ( 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 𝑝 ) ) ) ) ) )
65 64 2ralbidv ⊢ ( 𝑎 = ( ( ( 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 𝑝 ) ) ) ) ) )
66 65 anbi1d ⊢ ( 𝑎 = ( ( ( 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 ) ) ) )
67 66 biimpcd ⊢ ( ( ∀ 𝑝 ∈ 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 ⊢ ( ( ∀ 𝑝 ∈ 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 ⊢ ( ( ∀ 𝑝 ∈ 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 ⊢ ( ( ∀ 𝑝 ∈ 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 )
71 68 69 70 addsproplem3 ⊢ ( ( ∀ 𝑝 ∈ 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 ℎ ) } ) ) )
72 71 simp1d ⊢ ( ( ∀ 𝑝 ∈ 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 )
73 68 adantr ⊢ ( ( ( ∀ 𝑝 ∈ 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 𝑝 ) ) ) ) )
74 69 adantr ⊢ ( ( ( ∀ 𝑝 ∈ 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 )
75 70 adantr ⊢ ( ( ( ∀ 𝑝 ∈ 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 ⊢ ( ( ( ∀ 𝑝 ∈ 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 ⊢ ( ( ( ∀ 𝑝 ∈ 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 𝑧 )
78 73 74 75 76 77 addsproplem7 ⊢ ( ( ( ∀ 𝑝 ∈ 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 𝑥 ) )
79 78 ex ⊢ ( ( ∀ 𝑝 ∈ 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 𝑥 ) ) )
80 72 79 jca ⊢ ( ( ∀ 𝑝 ∈ 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 𝑥 ) ) ) )
81 67 80 syl6 ⊢ ( ( ∀ 𝑝 ∈ 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 𝑥 ) ) ) ) )
82 81 anassrs ⊢ ( ( ( ∀ 𝑝 ∈ 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 𝑥 ) ) ) ) )
83 82 ralrimiva ⊢ ( ( ∀ 𝑝 ∈ 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 𝑥 ) ) ) ) )
84 83 ralrimivva ⊢ ( ∀ 𝑝 ∈ 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 𝑥 ) ) ) ) )
85 61 84 sylbi ⊢ ( ∀ 𝑏 ∈ 𝑎 ∀ 𝑝 ∈ 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 𝑥 ) ) ) ) )
86 85 a1i ⊢ ( 𝑎 ∈ 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 𝑥 ) ) ) ) ) )
87 51 86 tfis2 ⊢ ( 𝑎 ∈ On → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( 𝑎 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
88 fveq2 ⊢ ( 𝑥 = 𝑋 → ( bday ‘ 𝑥 ) = ( bday ‘ 𝑋 ) )
89 88 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) )
90 88 oveq1d ⊢ ( 𝑥 = 𝑋 → ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) )
91 89 90 uneq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) )
92 91 eqeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑎 = ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) ) )
93 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 +s 𝑦 ) = ( 𝑋 +s 𝑦 ) )
94 93 eleq1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 +s 𝑦 ) ∈ No ↔ ( 𝑋 +s 𝑦 ) ∈ No ) )
95 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑦 +s 𝑥 ) = ( 𝑦 +s 𝑋 ) )
96 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑧 +s 𝑥 ) = ( 𝑧 +s 𝑋 ) )
97 95 96 breq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ↔ ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) )
98 97 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ↔ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) )
99 94 98 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ↔ ( ( 𝑋 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) ) )
100 92 99 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑎 = ( ( ( 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 ⊢ ( 𝑦 = 𝑌 → ( bday ‘ 𝑦 ) = ( bday ‘ 𝑌 ) )
102 101 oveq2d ⊢ ( 𝑦 = 𝑌 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
103 102 uneq1d ⊢ ( 𝑦 = 𝑌 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) )
104 103 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) ) )
105 oveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝑋 +s 𝑦 ) = ( 𝑋 +s 𝑌 ) )
106 105 eleq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 +s 𝑦 ) ∈ No ↔ ( 𝑋 +s 𝑌 ) ∈ No ) )
107 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 <s 𝑧 ↔ 𝑌 <s 𝑧 ) )
108 oveq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 +s 𝑋 ) = ( 𝑌 +s 𝑋 ) )
109 108 breq1d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ↔ ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) )
110 107 109 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ↔ ( 𝑌 <s 𝑧 → ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) )
111 106 110 anbi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝑋 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) ↔ ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑧 → ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) ) )
112 104 111 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑎 = ( ( ( 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 ⊢ ( 𝑧 = 𝑍 → ( bday ‘ 𝑧 ) = ( bday ‘ 𝑍 ) )
114 113 oveq2d ⊢ ( 𝑧 = 𝑍 → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) )
115 114 uneq2d ⊢ ( 𝑧 = 𝑍 → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
116 115 eqeq2d ⊢ ( 𝑧 = 𝑍 → ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) ↔ 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) ) )
117 breq2 ⊢ ( 𝑧 = 𝑍 → ( 𝑌 <s 𝑧 ↔ 𝑌 <s 𝑍 ) )
118 oveq1 ⊢ ( 𝑧 = 𝑍 → ( 𝑧 +s 𝑋 ) = ( 𝑍 +s 𝑋 ) )
119 118 breq2d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ↔ ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) )
120 117 119 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑌 <s 𝑧 → ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ↔ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) )
121 120 anbi2d ⊢ ( 𝑧 = 𝑍 → ( ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑧 → ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) ↔ ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) ) )
122 116 121 imbi12d ⊢ ( 𝑧 = 𝑍 → ( ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑧 ) ) ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑧 → ( 𝑌 +s 𝑋 ) <s ( 𝑧 +s 𝑋 ) ) ) ) ↔ ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) ) ) )
123 100 112 122 rspc3v ⊢ ( ( 𝑋 ∈ 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 𝑋 ) ) ) ) ) )
124 87 123 syl5com ⊢ ( 𝑎 ∈ On → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) ) ) )
125 124 com23 ⊢ ( 𝑎 ∈ On → ( 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) ) ) )
126 125 rexlimiv ⊢ ( ∃ 𝑎 ∈ On 𝑎 = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) ) )
127 10 126 ax-mp ⊢ ( ( 𝑋 ∈ No ∧ 𝑌 ∈ No ∧ 𝑍 ∈ No ) → ( ( 𝑋 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑍 → ( 𝑌 +s 𝑋 ) <s ( 𝑍 +s 𝑋 ) ) ) )