Proof of Theorem negsproplem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negsproplem1.1 | . . 3
⊢ (𝜑 → 𝑋 ∈  No
) | 
| 2 |  | negsproplem1.2 | . . 3
⊢ (𝜑 → 𝑌 ∈  No
) | 
| 3 | 1, 2 | jca 511 | . 2
⊢ (𝜑 → (𝑋 ∈  No 
∧ 𝑌 ∈  No )) | 
| 4 |  | negsproplem.1 | . 2
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 5 |  | negsproplem1.3 | . 2
⊢ (𝜑 → ((
bday ‘𝑋) ∪
( bday ‘𝑌)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) | 
| 6 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) | 
| 7 | 6 | uneq1d 4166 | . . . . 5
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) ∪
( bday ‘𝑦)) = (( bday
‘𝑋) ∪
( bday ‘𝑦))) | 
| 8 | 7 | eleq1d 2825 | . . . 4
⊢ (𝑥 = 𝑋 → ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) ↔ (( bday
‘𝑋) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)))) | 
| 9 |  | fveq2 6905 | . . . . . 6
⊢ (𝑥 = 𝑋 → ( -us ‘𝑥) = ( -us
‘𝑋)) | 
| 10 | 9 | eleq1d 2825 | . . . . 5
⊢ (𝑥 = 𝑋 → (( -us ‘𝑥) ∈ 
No  ↔ ( -us ‘𝑋) ∈  No
)) | 
| 11 |  | breq1 5145 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝑥 <s 𝑦 ↔ 𝑋 <s 𝑦)) | 
| 12 | 9 | breq2d 5154 | . . . . . 6
⊢ (𝑥 = 𝑋 → (( -us ‘𝑦) <s ( -us
‘𝑥) ↔ (
-us ‘𝑦)
<s ( -us ‘𝑋))) | 
| 13 | 11, 12 | imbi12d 344 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥)) ↔ (𝑋 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑋)))) | 
| 14 | 10, 13 | anbi12d 632 | . . . 4
⊢ (𝑥 = 𝑋 → ((( -us ‘𝑥) ∈ 
No  ∧ (𝑥 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑥)))
↔ (( -us ‘𝑋) ∈  No 
∧ (𝑋 <s 𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑋))))) | 
| 15 | 8, 14 | imbi12d 344 | . . 3
⊢ (𝑥 = 𝑋 → (((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝑥) ∈ 
No  ∧ (𝑥 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑥))))
↔ ((( bday ‘𝑋) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑋)
∈  No  ∧ (𝑋 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑋)))))) | 
| 16 |  | fveq2 6905 | . . . . . 6
⊢ (𝑦 = 𝑌 → ( bday
‘𝑦) = ( bday ‘𝑌)) | 
| 17 | 16 | uneq2d 4167 | . . . . 5
⊢ (𝑦 = 𝑌 → (( bday
‘𝑋) ∪
( bday ‘𝑦)) = (( bday
‘𝑋) ∪
( bday ‘𝑌))) | 
| 18 | 17 | eleq1d 2825 | . . . 4
⊢ (𝑦 = 𝑌 → ((( bday
‘𝑋) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) ↔ (( bday
‘𝑋) ∪
( bday ‘𝑌)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)))) | 
| 19 |  | breq2 5146 | . . . . . 6
⊢ (𝑦 = 𝑌 → (𝑋 <s 𝑦 ↔ 𝑋 <s 𝑌)) | 
| 20 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑌 → ( -us ‘𝑦) = ( -us
‘𝑌)) | 
| 21 | 20 | breq1d 5152 | . . . . . 6
⊢ (𝑦 = 𝑌 → (( -us ‘𝑦) <s ( -us
‘𝑋) ↔ (
-us ‘𝑌)
<s ( -us ‘𝑋))) | 
| 22 | 19, 21 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 𝑌 → ((𝑋 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑋)) ↔ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us
‘𝑋)))) | 
| 23 | 22 | anbi2d 630 | . . . 4
⊢ (𝑦 = 𝑌 → ((( -us ‘𝑋) ∈ 
No  ∧ (𝑋 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑋)))
↔ (( -us ‘𝑋) ∈  No 
∧ (𝑋 <s 𝑌 → ( -us
‘𝑌) <s (
-us ‘𝑋))))) | 
| 24 | 18, 23 | imbi12d 344 | . . 3
⊢ (𝑦 = 𝑌 → (((( bday
‘𝑋) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝑋) ∈ 
No  ∧ (𝑋 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑋))))
↔ ((( bday ‘𝑋) ∪ ( bday
‘𝑌)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑋)
∈  No  ∧ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us
‘𝑋)))))) | 
| 25 | 15, 24 | rspc2v 3632 | . 2
⊢ ((𝑋 ∈ 
No  ∧ 𝑌 ∈
 No ) → (∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥)))) →
((( bday ‘𝑋) ∪ ( bday
‘𝑌)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑋)
∈  No  ∧ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us
‘𝑋)))))) | 
| 26 | 3, 4, 5, 25 | syl3c 66 | 1
⊢ (𝜑 → (( -us
‘𝑋) ∈  No  ∧ (𝑋 <s 𝑌 → ( -us ‘𝑌) <s ( -us
‘𝑋)))) |