| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | addspropord.3 | . . . 4
⊢ (𝜑 → 𝑌 ∈  No
) | 
| 2 |  | addspropord.4 | . . . 4
⊢ (𝜑 → 𝑍 ∈  No
) | 
| 3 |  | addsproplem6.6 | . . . 4
⊢ (𝜑 → (
bday ‘𝑌) =
( bday ‘𝑍)) | 
| 4 |  | addspropord.5 | . . . 4
⊢ (𝜑 → 𝑌 <s 𝑍) | 
| 5 |  | nodense 27737 | . . . 4
⊢ (((𝑌 ∈ 
No  ∧ 𝑍 ∈
 No ) ∧ (( bday
‘𝑌) = ( bday ‘𝑍) ∧ 𝑌 <s 𝑍)) → ∃𝑚 ∈  No 
(( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍)) | 
| 6 | 1, 2, 3, 4, 5 | syl22anc 839 | . . 3
⊢ (𝜑 → ∃𝑚 ∈  No 
(( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍)) | 
| 7 |  | addsproplem.1 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ∀𝑧 ∈  No 
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈ 
No  ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) | 
| 8 |  | addspropord.2 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈  No
) | 
| 9 | 7, 8, 1 | addsproplem3 28004 | . . . . . 6
⊢ (𝜑 → ((𝑋 +s 𝑌) ∈  No 
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)}))) | 
| 10 | 9 | simp1d 1143 | . . . . 5
⊢ (𝜑 → (𝑋 +s 𝑌) ∈  No
) | 
| 11 | 10 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) ∈  No
) | 
| 12 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ∀𝑧 ∈  No 
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈ 
No  ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) | 
| 13 | 8 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑋 ∈  No
) | 
| 14 |  | simprl 771 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈  No
) | 
| 15 |  | unidm 4157 | . . . . . . 7
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑚))) =
(( bday ‘𝑋) +no ( bday
‘𝑚)) | 
| 16 |  | simprr1 1222 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑚) ∈
( bday ‘𝑌)) | 
| 17 |  | bdayelon 27821 | . . . . . . . . . 10
⊢ ( bday ‘𝑚) ∈ On | 
| 18 |  | bdayelon 27821 | . . . . . . . . . 10
⊢ ( bday ‘𝑌) ∈ On | 
| 19 |  | bdayelon 27821 | . . . . . . . . . 10
⊢ ( bday ‘𝑋) ∈ On | 
| 20 |  | naddel2 8726 | . . . . . . . . . 10
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑚)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) | 
| 21 | 17, 18, 19, 20 | mp3an 1463 | . . . . . . . . 9
⊢ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) | 
| 22 | 16, 21 | sylib 218 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) | 
| 23 |  | elun1 4182 | . . . . . . . 8
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) | 
| 24 | 22, 23 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) | 
| 25 | 15, 24 | eqeltrid 2845 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑚))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) | 
| 26 | 12, 13, 14, 14, 25 | addsproplem1 28002 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((𝑋 +s 𝑚) ∈  No 
∧ (𝑚 <s 𝑚 → (𝑚 +s 𝑋) <s (𝑚 +s 𝑋)))) | 
| 27 | 26 | simpld 494 | . . . 4
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈  No
) | 
| 28 |  | uncom 4158 | . . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) =
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) | 
| 29 | 28 | eleq2i 2833 | . . . . . . . . . . 11
⊢ (((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) ↔
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌)))) | 
| 30 | 29 | imbi1i 349 | . . . . . . . . . 10
⊢
((((( 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 𝑥))))) | 
| 31 | 30 | ralbii 3093 | . . . . . . . . 9
⊢
(∀𝑧 ∈
 No  (((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ∈ ((( 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 𝑥))))) | 
| 32 | 31 | 2ralbii 3128 | . . . . . . . 8
⊢
(∀𝑥 ∈
 No  ∀𝑦 ∈  No 
∀𝑧 ∈  No  (((( bday ‘𝑥) +no (
bday ‘𝑦))
∪ (( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( 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 𝑥))))) | 
| 33 | 7, 32 | sylib 218 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ∀𝑧 ∈  No 
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈ 
No  ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) | 
| 34 | 33, 8, 2 | addsproplem3 28004 | . . . . . 6
⊢ (𝜑 → ((𝑋 +s 𝑍) ∈  No 
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)} ∧ {(𝑋 +s 𝑍)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑍)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑍)𝑔 = (𝑋 +s ℎ)}))) | 
| 35 | 34 | simp1d 1143 | . . . . 5
⊢ (𝜑 → (𝑋 +s 𝑍) ∈  No
) | 
| 36 | 35 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑍) ∈  No
) | 
| 37 | 9 | simp3d 1145 | . . . . . 6
⊢ (𝜑 → {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) | 
| 38 | 37 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) | 
| 39 |  | ovex 7464 | . . . . . . 7
⊢ (𝑋 +s 𝑌) ∈ V | 
| 40 | 39 | snid 4662 | . . . . . 6
⊢ (𝑋 +s 𝑌) ∈ {(𝑋 +s 𝑌)} | 
| 41 | 40 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) ∈ {(𝑋 +s 𝑌)}) | 
| 42 |  | oldbday 27939 | . . . . . . . . . . 11
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈  No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑌))) | 
| 43 | 18, 14, 42 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑌))) | 
| 44 | 16, 43 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( O ‘(
bday ‘𝑌))) | 
| 45 |  | simprr2 1223 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑌 <s 𝑚) | 
| 46 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (𝑌 <s 𝑎 ↔ 𝑌 <s 𝑚)) | 
| 47 |  | rightval 27903 | . . . . . . . . . 10
⊢ ( R
‘𝑌) = {𝑎 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑎} | 
| 48 | 46, 47 | elrab2 3695 | . . . . . . . . 9
⊢ (𝑚 ∈ ( R ‘𝑌) ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑌 <s 𝑚)) | 
| 49 | 44, 45, 48 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( R ‘𝑌)) | 
| 50 |  | eqid 2737 | . . . . . . . 8
⊢ (𝑋 +s 𝑚) = (𝑋 +s 𝑚) | 
| 51 |  | oveq2 7439 | . . . . . . . . 9
⊢ (ℎ = 𝑚 → (𝑋 +s ℎ) = (𝑋 +s 𝑚)) | 
| 52 | 51 | rspceeqv 3645 | . . . . . . . 8
⊢ ((𝑚 ∈ ( R ‘𝑌) ∧ (𝑋 +s 𝑚) = (𝑋 +s 𝑚)) → ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) | 
| 53 | 49, 50, 52 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) | 
| 54 |  | ovex 7464 | . . . . . . . 8
⊢ (𝑋 +s 𝑚) ∈ V | 
| 55 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑔 = (𝑋 +s 𝑚) → (𝑔 = (𝑋 +s ℎ) ↔ (𝑋 +s 𝑚) = (𝑋 +s ℎ))) | 
| 56 | 55 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑔 = (𝑋 +s 𝑚) → (∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ) ↔ ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ))) | 
| 57 | 54, 56 | elab 3679 | . . . . . . 7
⊢ ((𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)} ↔ ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) | 
| 58 | 53, 57 | sylibr 234 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)}) | 
| 59 |  | elun2 4183 | . . . . . 6
⊢ ((𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)} → (𝑋 +s 𝑚) ∈ ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) | 
| 60 | 58, 59 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) | 
| 61 | 38, 41, 60 | ssltsepcd 27839 | . . . 4
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) <s (𝑋 +s 𝑚)) | 
| 62 | 33 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ∀𝑧 ∈  No 
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈ 
No  ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) | 
| 63 | 2 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑍 ∈  No
) | 
| 64 | 62, 13, 63 | addsproplem3 28004 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((𝑋 +s 𝑍) ∈  No 
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)} ∧ {(𝑋 +s 𝑍)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑍)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑍)𝑔 = (𝑋 +s ℎ)}))) | 
| 65 | 64 | simp2d 1144 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)}) | 
| 66 | 3 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑌) = ( bday ‘𝑍)) | 
| 67 | 16, 66 | eleqtrd 2843 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑚) ∈
( bday ‘𝑍)) | 
| 68 |  | bdayelon 27821 | . . . . . . . . . . 11
⊢ ( bday ‘𝑍) ∈ On | 
| 69 |  | oldbday 27939 | . . . . . . . . . . 11
⊢ ((( bday ‘𝑍) ∈ On ∧ 𝑚 ∈  No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑍)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑍))) | 
| 70 | 68, 14, 69 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑚 ∈ ( O ‘(
bday ‘𝑍))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑍))) | 
| 71 | 67, 70 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( O ‘(
bday ‘𝑍))) | 
| 72 |  | simprr3 1224 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 <s 𝑍) | 
| 73 |  | breq1 5146 | . . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (𝑎 <s 𝑍 ↔ 𝑚 <s 𝑍)) | 
| 74 |  | leftval 27902 | . . . . . . . . . 10
⊢ ( L
‘𝑍) = {𝑎 ∈ ( O ‘( bday ‘𝑍)) ∣ 𝑎 <s 𝑍} | 
| 75 | 73, 74 | elrab2 3695 | . . . . . . . . 9
⊢ (𝑚 ∈ ( L ‘𝑍) ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑍))
∧ 𝑚 <s 𝑍)) | 
| 76 | 71, 72, 75 | sylanbrc 583 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( L ‘𝑍)) | 
| 77 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑑 = 𝑚 → (𝑋 +s 𝑑) = (𝑋 +s 𝑚)) | 
| 78 | 77 | rspceeqv 3645 | . . . . . . . 8
⊢ ((𝑚 ∈ ( L ‘𝑍) ∧ (𝑋 +s 𝑚) = (𝑋 +s 𝑚)) → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) | 
| 79 | 76, 50, 78 | sylancl 586 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) | 
| 80 |  | eqeq1 2741 | . . . . . . . . 9
⊢ (𝑐 = (𝑋 +s 𝑚) → (𝑐 = (𝑋 +s 𝑑) ↔ (𝑋 +s 𝑚) = (𝑋 +s 𝑑))) | 
| 81 | 80 | rexbidv 3179 | . . . . . . . 8
⊢ (𝑐 = (𝑋 +s 𝑚) → (∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑) ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑))) | 
| 82 | 54, 81 | elab 3679 | . . . . . . 7
⊢ ((𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)} ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) | 
| 83 | 79, 82 | sylibr 234 | . . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) | 
| 84 |  | elun2 4183 | . . . . . 6
⊢ ((𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)} → (𝑋 +s 𝑚) ∈ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)})) | 
| 85 | 83, 84 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)})) | 
| 86 |  | ovex 7464 | . . . . . . 7
⊢ (𝑋 +s 𝑍) ∈ V | 
| 87 | 86 | snid 4662 | . . . . . 6
⊢ (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)} | 
| 88 | 87 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)}) | 
| 89 | 65, 85, 88 | ssltsepcd 27839 | . . . 4
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑍)) | 
| 90 | 11, 27, 36, 61, 89 | slttrd 27804 | . . 3
⊢ ((𝜑 ∧ (𝑚 ∈  No 
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) <s (𝑋 +s 𝑍)) | 
| 91 | 6, 90 | rexlimddv 3161 | . 2
⊢ (𝜑 → (𝑋 +s 𝑌) <s (𝑋 +s 𝑍)) | 
| 92 | 1, 8 | addscomd 28000 | . 2
⊢ (𝜑 → (𝑌 +s 𝑋) = (𝑋 +s 𝑌)) | 
| 93 | 2, 8 | addscomd 28000 | . 2
⊢ (𝜑 → (𝑍 +s 𝑋) = (𝑋 +s 𝑍)) | 
| 94 | 91, 92, 93 | 3brtr4d 5175 | 1
⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |