| Step | Hyp | Ref
| Expression |
| 1 | | leftval 27902 |
. . . . 5
⊢ ( L
‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} |
| 2 | | rightval 27903 |
. . . . 5
⊢ ( R
‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥} |
| 3 | 1, 2 | uneq12i 4166 |
. . . 4
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ 𝐴 <s 𝑥}) |
| 4 | | unrab 4315 |
. . . 4
⊢ ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ 𝐴 <s 𝑥}) = {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} |
| 5 | 3, 4 | eqtri 2765 |
. . 3
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} |
| 6 | | oldirr 27928 |
. . . . . . . 8
⊢ ¬
𝐴 ∈ ( O ‘( bday ‘𝐴)) |
| 7 | | eleq1 2829 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ( O ‘(
bday ‘𝐴))
↔ 𝐴 ∈ ( O
‘( bday ‘𝐴)))) |
| 8 | 6, 7 | mtbiri 327 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ¬ 𝑥 ∈ ( O ‘(
bday ‘𝐴))) |
| 9 | 8 | necon2ai 2970 |
. . . . . 6
⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ≠ 𝐴) |
| 10 | 9 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → 𝑥 ≠ 𝐴) |
| 11 | | oldssno 27900 |
. . . . . . 7
⊢ ( O
‘( bday ‘𝐴)) ⊆ No
|
| 12 | 11 | sseli 3979 |
. . . . . 6
⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ∈ No
) |
| 13 | | slttrine 27796 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ 𝐴 ∈
No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
| 14 | 13 | ancoms 458 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
| 15 | 12, 14 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
| 16 | 10, 15 | mpbid 232 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)) |
| 17 | 16 | rabeqcda 3448 |
. . 3
⊢ (𝐴 ∈
No → {𝑥 ∈
( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} = ( O ‘( bday
‘𝐴))) |
| 18 | 5, 17 | eqtrid 2789 |
. 2
⊢ (𝐴 ∈
No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday
‘𝐴))) |
| 19 | | un0 4394 |
. . 3
⊢ (∅
∪ ∅) = ∅ |
| 20 | | leftf 27904 |
. . . . . . 7
⊢ L : No ⟶𝒫 No
|
| 21 | 20 | fdmi 6747 |
. . . . . 6
⊢ dom L =
No |
| 22 | 21 | eleq2i 2833 |
. . . . 5
⊢ (𝐴 ∈ dom L ↔ 𝐴 ∈
No ) |
| 23 | | ndmfv 6941 |
. . . . 5
⊢ (¬
𝐴 ∈ dom L → ( L
‘𝐴) =
∅) |
| 24 | 22, 23 | sylnbir 331 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( L ‘𝐴) = ∅) |
| 25 | | rightf 27905 |
. . . . . . 7
⊢ R : No ⟶𝒫 No
|
| 26 | 25 | fdmi 6747 |
. . . . . 6
⊢ dom R =
No |
| 27 | 26 | eleq2i 2833 |
. . . . 5
⊢ (𝐴 ∈ dom R ↔ 𝐴 ∈
No ) |
| 28 | | ndmfv 6941 |
. . . . 5
⊢ (¬
𝐴 ∈ dom R → ( R
‘𝐴) =
∅) |
| 29 | 27, 28 | sylnbir 331 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( R ‘𝐴) = ∅) |
| 30 | 24, 29 | uneq12d 4169 |
. . 3
⊢ (¬
𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = (∅ ∪
∅)) |
| 31 | | bdaydm 27819 |
. . . . . . 7
⊢ dom bday = No
|
| 32 | 31 | eleq2i 2833 |
. . . . . 6
⊢ (𝐴 ∈ dom bday ↔ 𝐴 ∈ No
) |
| 33 | | ndmfv 6941 |
. . . . . 6
⊢ (¬
𝐴 ∈ dom bday → ( bday
‘𝐴) =
∅) |
| 34 | 32, 33 | sylnbir 331 |
. . . . 5
⊢ (¬
𝐴 ∈ No → ( bday
‘𝐴) =
∅) |
| 35 | 34 | fveq2d 6910 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( O ‘( bday
‘𝐴)) = ( O
‘∅)) |
| 36 | | old0 27898 |
. . . 4
⊢ ( O
‘∅) = ∅ |
| 37 | 35, 36 | eqtrdi 2793 |
. . 3
⊢ (¬
𝐴 ∈ No → ( O ‘( bday
‘𝐴)) =
∅) |
| 38 | 19, 30, 37 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday
‘𝐴))) |
| 39 | 18, 38 | pm2.61i 182 |
1
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = ( O
‘( bday ‘𝐴)) |