| Step | Hyp | Ref
| Expression |
| 1 | | oldssno 27900 |
. . . . . . . . . . . 12
⊢ ( O
‘( bday ‘𝑋)) ⊆ No
|
| 2 | 1 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ( O ‘( bday ‘𝑋)) → 𝑥 ∈ No
) |
| 3 | 2 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑥 ∈ No
) |
| 4 | | simp1l1 1267 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑋 ∈ No
) |
| 5 | | simp1l2 1268 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑌 ∈ No
) |
| 6 | | simp3 1139 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑥 <s 𝑋) |
| 7 | | simp1r 1199 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑋 <s 𝑌) |
| 8 | 3, 4, 5, 6, 7 | slttrd 27804 |
. . . . . . . . 9
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ 𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → 𝑥 <s 𝑌) |
| 9 | 8 | 3exp 1120 |
. . . . . . . 8
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( O ‘(
bday ‘𝑋))
→ (𝑥 <s 𝑋 → 𝑥 <s 𝑌))) |
| 10 | 9 | imdistand 570 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑌))) |
| 11 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) = ( bday
‘𝑌) → ( O
‘( bday ‘𝑋)) = ( O ‘( bday
‘𝑌))) |
| 12 | 11 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → ( O ‘(
bday ‘𝑋)) = (
O ‘( bday ‘𝑌))) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( O ‘(
bday ‘𝑋)) = (
O ‘( bday ‘𝑌))) |
| 14 | 13 | eleq2d 2827 |
. . . . . . . 8
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( O ‘(
bday ‘𝑋))
↔ 𝑥 ∈ ( O
‘( bday ‘𝑌)))) |
| 15 | 14 | anbi1d 631 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑌) ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌))) |
| 16 | 10, 15 | sylibd 239 |
. . . . . 6
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ((𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋) → (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌))) |
| 17 | | leftval 27902 |
. . . . . . . . 9
⊢ ( L
‘𝑋) = {𝑥 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑥 <s 𝑋} |
| 18 | 17 | a1i 11 |
. . . . . . . 8
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) = {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋}) |
| 19 | 18 | eleq2d 2827 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋})) |
| 20 | | rabid 3458 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋} ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋)) |
| 21 | 19, 20 | bitrdi 287 |
. . . . . 6
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑥 <s 𝑋))) |
| 22 | | leftval 27902 |
. . . . . . . . 9
⊢ ( L
‘𝑌) = {𝑥 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑥 <s 𝑌} |
| 23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑌) = {𝑥 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑥 <s 𝑌}) |
| 24 | 23 | eleq2d 2827 |
. . . . . . 7
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑌) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑥 <s 𝑌})) |
| 25 | | rabid 3458 |
. . . . . . 7
⊢ (𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑥 <s 𝑌} ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) |
| 26 | 24, 25 | bitrdi 287 |
. . . . . 6
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑌) ↔ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌))) |
| 27 | 16, 21, 26 | 3imtr4d 294 |
. . . . 5
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (𝑥 ∈ ( L ‘𝑋) → 𝑥 ∈ ( L ‘𝑌))) |
| 28 | 27 | ssrdv 3989 |
. . . 4
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊆ ( L ‘𝑌)) |
| 29 | | sltirr 27791 |
. . . . . . . . 9
⊢ (𝑌 ∈
No → ¬ 𝑌
<s 𝑌) |
| 30 | 29 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → ¬ 𝑌 <s 𝑌) |
| 31 | | breq1 5146 |
. . . . . . . . 9
⊢ (𝑋 = 𝑌 → (𝑋 <s 𝑌 ↔ 𝑌 <s 𝑌)) |
| 32 | 31 | notbid 318 |
. . . . . . . 8
⊢ (𝑋 = 𝑌 → (¬ 𝑋 <s 𝑌 ↔ ¬ 𝑌 <s 𝑌)) |
| 33 | 30, 32 | syl5ibrcom 247 |
. . . . . . 7
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (𝑋 = 𝑌 → ¬ 𝑋 <s 𝑌)) |
| 34 | 33 | con2d 134 |
. . . . . 6
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ¬ 𝑋 = 𝑌)) |
| 35 | 34 | imp 406 |
. . . . 5
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ¬ 𝑋 = 𝑌) |
| 36 | | simpr 484 |
. . . . . . 7
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( L ‘𝑋) = ( L ‘𝑌)) |
| 37 | | lruneq 27944 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌))) |
| 38 | 37 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌))) |
| 39 | 38 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) ∪ ( R ‘𝑋)) = (( L ‘𝑌) ∪ ( R ‘𝑌))) |
| 40 | 39, 36 | difeq12d 4127 |
. . . . . . . 8
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌))) |
| 41 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((( L
‘𝑋) ∪ ( R
‘𝑋)) ∖ ( L
‘𝑋)) = ((( L
‘𝑋) ∖ ( L
‘𝑋)) ∪ (( R
‘𝑋) ∖ ( L
‘𝑋))) |
| 42 | | difid 4376 |
. . . . . . . . . . 11
⊢ (( L
‘𝑋) ∖ ( L
‘𝑋)) =
∅ |
| 43 | 42 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ((( L
‘𝑋) ∖ ( L
‘𝑋)) ∪ (( R
‘𝑋) ∖ ( L
‘𝑋))) = (∅
∪ (( R ‘𝑋)
∖ ( L ‘𝑋))) |
| 44 | | 0un 4396 |
. . . . . . . . . 10
⊢ (∅
∪ (( R ‘𝑋)
∖ ( L ‘𝑋))) =
(( R ‘𝑋) ∖ ( L
‘𝑋)) |
| 45 | 41, 43, 44 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((( L
‘𝑋) ∪ ( R
‘𝑋)) ∖ ( L
‘𝑋)) = (( R
‘𝑋) ∖ ( L
‘𝑋)) |
| 46 | | incom 4209 |
. . . . . . . . . . 11
⊢ (( L
‘𝑋) ∩ ( R
‘𝑋)) = (( R
‘𝑋) ∩ ( L
‘𝑋)) |
| 47 | | lltropt 27911 |
. . . . . . . . . . . 12
⊢ ( L
‘𝑋) <<s ( R
‘𝑋) |
| 48 | | ssltdisj 27866 |
. . . . . . . . . . . 12
⊢ (( L
‘𝑋) <<s ( R
‘𝑋) → (( L
‘𝑋) ∩ ( R
‘𝑋)) =
∅) |
| 49 | 47, 48 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) ∩ ( R ‘𝑋)) = ∅) |
| 50 | 46, 49 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∩ ( L ‘𝑋)) = ∅) |
| 51 | | disjdif2 4480 |
. . . . . . . . . 10
⊢ ((( R
‘𝑋) ∩ ( L
‘𝑋)) = ∅ →
(( R ‘𝑋) ∖ ( L
‘𝑋)) = ( R
‘𝑋)) |
| 52 | 50, 51 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑋) ∖ ( L ‘𝑋)) = ( R ‘𝑋)) |
| 53 | 45, 52 | eqtrid 2789 |
. . . . . . . 8
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑋) ∪ ( R ‘𝑋)) ∖ ( L ‘𝑋)) = ( R ‘𝑋)) |
| 54 | | difundir 4291 |
. . . . . . . . . 10
⊢ ((( L
‘𝑌) ∪ ( R
‘𝑌)) ∖ ( L
‘𝑌)) = ((( L
‘𝑌) ∖ ( L
‘𝑌)) ∪ (( R
‘𝑌) ∖ ( L
‘𝑌))) |
| 55 | | difid 4376 |
. . . . . . . . . . 11
⊢ (( L
‘𝑌) ∖ ( L
‘𝑌)) =
∅ |
| 56 | 55 | uneq1i 4164 |
. . . . . . . . . 10
⊢ ((( L
‘𝑌) ∖ ( L
‘𝑌)) ∪ (( R
‘𝑌) ∖ ( L
‘𝑌))) = (∅
∪ (( R ‘𝑌)
∖ ( L ‘𝑌))) |
| 57 | | 0un 4396 |
. . . . . . . . . 10
⊢ (∅
∪ (( R ‘𝑌)
∖ ( L ‘𝑌))) =
(( R ‘𝑌) ∖ ( L
‘𝑌)) |
| 58 | 54, 56, 57 | 3eqtri 2769 |
. . . . . . . . 9
⊢ ((( L
‘𝑌) ∪ ( R
‘𝑌)) ∖ ( L
‘𝑌)) = (( R
‘𝑌) ∖ ( L
‘𝑌)) |
| 59 | | incom 4209 |
. . . . . . . . . . 11
⊢ (( L
‘𝑌) ∩ ( R
‘𝑌)) = (( R
‘𝑌) ∩ ( L
‘𝑌)) |
| 60 | | lltropt 27911 |
. . . . . . . . . . . 12
⊢ ( L
‘𝑌) <<s ( R
‘𝑌) |
| 61 | | ssltdisj 27866 |
. . . . . . . . . . . 12
⊢ (( L
‘𝑌) <<s ( R
‘𝑌) → (( L
‘𝑌) ∩ ( R
‘𝑌)) =
∅) |
| 62 | 60, 61 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) ∩ ( R ‘𝑌)) = ∅) |
| 63 | 59, 62 | eqtr3id 2791 |
. . . . . . . . . 10
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∩ ( L ‘𝑌)) = ∅) |
| 64 | | disjdif2 4480 |
. . . . . . . . . 10
⊢ ((( R
‘𝑌) ∩ ( L
‘𝑌)) = ∅ →
(( R ‘𝑌) ∖ ( L
‘𝑌)) = ( R
‘𝑌)) |
| 65 | 63, 64 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( R ‘𝑌) ∖ ( L ‘𝑌)) = ( R ‘𝑌)) |
| 66 | 58, 65 | eqtrid 2789 |
. . . . . . . 8
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ((( L ‘𝑌) ∪ ( R ‘𝑌)) ∖ ( L ‘𝑌)) = ( R ‘𝑌)) |
| 67 | 40, 53, 66 | 3eqtr3d 2785 |
. . . . . . 7
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → ( R ‘𝑋) = ( R ‘𝑌)) |
| 68 | 36, 67 | oveq12d 7449 |
. . . . . 6
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = (( L ‘𝑌) |s ( R ‘𝑌))) |
| 69 | | simpll1 1213 |
. . . . . . 7
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 ∈ No
) |
| 70 | | lrcut 27941 |
. . . . . . 7
⊢ (𝑋 ∈
No → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) |
| 71 | 69, 70 | syl 17 |
. . . . . 6
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑋) |s ( R ‘𝑋)) = 𝑋) |
| 72 | | simpll2 1214 |
. . . . . . 7
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑌 ∈ No
) |
| 73 | | lrcut 27941 |
. . . . . . 7
⊢ (𝑌 ∈
No → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌) |
| 74 | 72, 73 | syl 17 |
. . . . . 6
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → (( L ‘𝑌) |s ( R ‘𝑌)) = 𝑌) |
| 75 | 68, 71, 74 | 3eqtr3d 2785 |
. . . . 5
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) ∧ ( L ‘𝑋) = ( L ‘𝑌)) → 𝑋 = 𝑌) |
| 76 | 35, 75 | mtand 816 |
. . . 4
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ¬ ( L ‘𝑋) = ( L ‘𝑌)) |
| 77 | | dfpss2 4088 |
. . . 4
⊢ (( L
‘𝑋) ⊊ ( L
‘𝑌) ↔ (( L
‘𝑋) ⊆ ( L
‘𝑌) ∧ ¬ ( L
‘𝑋) = ( L
‘𝑌))) |
| 78 | 28, 76, 77 | sylanbrc 583 |
. . 3
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ 𝑋 <s 𝑌) → ( L ‘𝑋) ⊊ ( L ‘𝑌)) |
| 79 | 78 | ex 412 |
. 2
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 → ( L ‘𝑋) ⊊ ( L ‘𝑌))) |
| 80 | | dfpss3 4089 |
. . 3
⊢ (( L
‘𝑋) ⊊ ( L
‘𝑌) ↔ (( L
‘𝑋) ⊆ ( L
‘𝑌) ∧ ¬ ( L
‘𝑌) ⊆ ( L
‘𝑋))) |
| 81 | | ssdif0 4366 |
. . . . . . 7
⊢ (( L
‘𝑌) ⊆ ( L
‘𝑋) ↔ (( L
‘𝑌) ∖ ( L
‘𝑋)) =
∅) |
| 82 | 81 | necon3bbii 2988 |
. . . . . 6
⊢ (¬ (
L ‘𝑌) ⊆ ( L
‘𝑋) ↔ (( L
‘𝑌) ∖ ( L
‘𝑋)) ≠
∅) |
| 83 | | n0 4353 |
. . . . . 6
⊢ ((( L
‘𝑌) ∖ ( L
‘𝑋)) ≠ ∅
↔ ∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋))) |
| 84 | 82, 83 | bitri 275 |
. . . . 5
⊢ (¬ (
L ‘𝑌) ⊆ ( L
‘𝑋) ↔
∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋))) |
| 85 | | eldif 3961 |
. . . . . . 7
⊢ (𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) ↔ (𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋))) |
| 86 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈
No → ( L ‘𝑌) = {𝑥 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑥 <s 𝑌}) |
| 87 | 86 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑌 ∈
No → (𝑥 ∈
( L ‘𝑌) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑥 <s 𝑌})) |
| 88 | 87, 25 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑌 ∈
No → (𝑥 ∈
( L ‘𝑌) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑥 <s 𝑌))) |
| 89 | 17 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈
No → ( L ‘𝑋) = {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋}) |
| 90 | 89 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → (𝑥 ∈
( L ‘𝑋) ↔ 𝑥 ∈ {𝑥 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑥 <s 𝑋})) |
| 91 | 90, 20 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈
No → (𝑥 ∈
( L ‘𝑋) ↔ (𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))) |
| 92 | 91 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑋 ∈
No → (¬ 𝑥
∈ ( L ‘𝑋) ↔
¬ (𝑥 ∈ ( O
‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋))) |
| 93 | | ianor 984 |
. . . . . . . . . . 11
⊢ (¬
(𝑥 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑥 <s 𝑋) ↔ (¬ 𝑥 ∈ ( O ‘(
bday ‘𝑋)) ∨
¬ 𝑥 <s 𝑋)) |
| 94 | 92, 93 | bitrdi 287 |
. . . . . . . . . 10
⊢ (𝑋 ∈
No → (¬ 𝑥
∈ ( L ‘𝑋) ↔
(¬ 𝑥 ∈ ( O
‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋))) |
| 95 | 88, 94 | bi2anan9r 639 |
. . . . . . . . 9
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) ↔ ((𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋)))) |
| 96 | 95 | 3adant3 1133 |
. . . . . . . 8
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) ↔ ((𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋)))) |
| 97 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → 𝑥 ∈ ( O ‘(
bday ‘𝑌))) |
| 98 | | simpl3 1194 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → ( bday ‘𝑋) = ( bday
‘𝑌)) |
| 99 | 98 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → ( O ‘( bday ‘𝑋)) = ( O ‘( bday
‘𝑌))) |
| 100 | 97, 99 | eleqtrrd 2844 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → 𝑥 ∈ ( O ‘(
bday ‘𝑋))) |
| 101 | 100 | pm2.24d 151 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) → 𝑋 <s 𝑌)) |
| 102 | | simpll1 1213 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 ∈ No
) |
| 103 | | oldssno 27900 |
. . . . . . . . . . . . . 14
⊢ ( O
‘( bday ‘𝑌)) ⊆ No
|
| 104 | 103, 97 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → 𝑥 ∈ No
) |
| 105 | 104 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑥 ∈ No
) |
| 106 | | simpll2 1214 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑌 ∈ No
) |
| 107 | | simpl1 1192 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → 𝑋 ∈ No
) |
| 108 | | slenlt 27797 |
. . . . . . . . . . . . . 14
⊢ ((𝑋 ∈
No ∧ 𝑥 ∈
No ) → (𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋)) |
| 109 | 107, 104,
108 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → (𝑋 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑋)) |
| 110 | 109 | biimpar 477 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 ≤s 𝑥) |
| 111 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑥 <s 𝑌) |
| 112 | 102, 105,
106, 110, 111 | slelttrd 27806 |
. . . . . . . . . . 11
⊢ ((((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) ∧ ¬ 𝑥 <s 𝑋) → 𝑋 <s 𝑌) |
| 113 | 112 | ex 412 |
. . . . . . . . . 10
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → (¬ 𝑥 <s 𝑋 → 𝑋 <s 𝑌)) |
| 114 | 101, 113 | jaod 860 |
. . . . . . . . 9
⊢ (((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) ∧ (𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌)) → ((¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋) → 𝑋 <s 𝑌)) |
| 115 | 114 | expimpd 453 |
. . . . . . . 8
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (((𝑥 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑥 <s 𝑌) ∧ (¬ 𝑥 ∈ ( O ‘( bday ‘𝑋)) ∨ ¬ 𝑥 <s 𝑋)) → 𝑋 <s 𝑌)) |
| 116 | 96, 115 | sylbid 240 |
. . . . . . 7
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → ((𝑥 ∈ ( L ‘𝑌) ∧ ¬ 𝑥 ∈ ( L ‘𝑋)) → 𝑋 <s 𝑌)) |
| 117 | 85, 116 | biimtrid 242 |
. . . . . 6
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌)) |
| 118 | 117 | exlimdv 1933 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (∃𝑥 𝑥 ∈ (( L ‘𝑌) ∖ ( L ‘𝑋)) → 𝑋 <s 𝑌)) |
| 119 | 84, 118 | biimtrid 242 |
. . . 4
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (¬ ( L ‘𝑌) ⊆ ( L ‘𝑋) → 𝑋 <s 𝑌)) |
| 120 | 119 | adantld 490 |
. . 3
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → ((( L ‘𝑋) ⊆ ( L ‘𝑌) ∧ ¬ ( L ‘𝑌) ⊆ ( L ‘𝑋)) → 𝑋 <s 𝑌)) |
| 121 | 80, 120 | biimtrid 242 |
. 2
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (( L ‘𝑋) ⊊ ( L ‘𝑌) → 𝑋 <s 𝑌)) |
| 122 | 79, 121 | impbid 212 |
1
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ ( bday
‘𝑋) = ( bday ‘𝑌)) → (𝑋 <s 𝑌 ↔ ( L ‘𝑋) ⊊ ( L ‘𝑌))) |