Step | Hyp | Ref
| Expression |
1 | | leftval 34047 |
. . . . 5
⊢ ( L
‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} |
2 | | rightval 34048 |
. . . . 5
⊢ ( R
‘𝐴) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑥} |
3 | 1, 2 | uneq12i 4095 |
. . . 4
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ 𝐴 <s 𝑥}) |
4 | | unrab 4239 |
. . . 4
⊢ ({𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝑥 <s 𝐴} ∪ {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ 𝐴 <s 𝑥}) = {𝑥 ∈ ( O ‘(
bday ‘𝐴))
∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} |
5 | 3, 4 | eqtri 2766 |
. . 3
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = {𝑥 ∈ ( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} |
6 | | oldirr 34072 |
. . . . . . . 8
⊢ ¬
𝐴 ∈ ( O ‘( bday ‘𝐴)) |
7 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ ( O ‘(
bday ‘𝐴))
↔ 𝐴 ∈ ( O
‘( bday ‘𝐴)))) |
8 | 6, 7 | mtbiri 327 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ¬ 𝑥 ∈ ( O ‘(
bday ‘𝐴))) |
9 | 8 | necon2ai 2973 |
. . . . . 6
⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ≠ 𝐴) |
10 | 9 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → 𝑥 ≠ 𝐴) |
11 | | oldssno 34045 |
. . . . . . 7
⊢ ( O
‘( bday ‘𝐴)) ⊆ No
|
12 | 11 | sseli 3917 |
. . . . . 6
⊢ (𝑥 ∈ ( O ‘( bday ‘𝐴)) → 𝑥 ∈ No
) |
13 | | slttrine 33954 |
. . . . . . 7
⊢ ((𝑥 ∈
No ∧ 𝐴 ∈
No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
14 | 13 | ancoms 459 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈
No ) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
15 | 12, 14 | sylan2 593 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → (𝑥 ≠ 𝐴 ↔ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥))) |
16 | 10, 15 | mpbid 231 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝑥 ∈ (
O ‘( bday ‘𝐴))) → (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)) |
17 | 16 | rabeqcda 3429 |
. . 3
⊢ (𝐴 ∈
No → {𝑥 ∈
( O ‘( bday ‘𝐴)) ∣ (𝑥 <s 𝐴 ∨ 𝐴 <s 𝑥)} = ( O ‘( bday
‘𝐴))) |
18 | 5, 17 | eqtrid 2790 |
. 2
⊢ (𝐴 ∈
No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday
‘𝐴))) |
19 | | un0 4324 |
. . 3
⊢ (∅
∪ ∅) = ∅ |
20 | | leftf 34049 |
. . . . . . 7
⊢ L : No ⟶𝒫 No
|
21 | 20 | fdmi 6612 |
. . . . . 6
⊢ dom L =
No |
22 | 21 | eleq2i 2830 |
. . . . 5
⊢ (𝐴 ∈ dom L ↔ 𝐴 ∈
No ) |
23 | | ndmfv 6804 |
. . . . 5
⊢ (¬
𝐴 ∈ dom L → ( L
‘𝐴) =
∅) |
24 | 22, 23 | sylnbir 331 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( L ‘𝐴) = ∅) |
25 | | rightf 34050 |
. . . . . . 7
⊢ R : No ⟶𝒫 No
|
26 | 25 | fdmi 6612 |
. . . . . 6
⊢ dom R =
No |
27 | 26 | eleq2i 2830 |
. . . . 5
⊢ (𝐴 ∈ dom R ↔ 𝐴 ∈
No ) |
28 | | ndmfv 6804 |
. . . . 5
⊢ (¬
𝐴 ∈ dom R → ( R
‘𝐴) =
∅) |
29 | 27, 28 | sylnbir 331 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( R ‘𝐴) = ∅) |
30 | 24, 29 | uneq12d 4098 |
. . 3
⊢ (¬
𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = (∅ ∪
∅)) |
31 | | bdaydm 33969 |
. . . . . . 7
⊢ dom bday = No
|
32 | 31 | eleq2i 2830 |
. . . . . 6
⊢ (𝐴 ∈ dom bday ↔ 𝐴 ∈ No
) |
33 | | ndmfv 6804 |
. . . . . 6
⊢ (¬
𝐴 ∈ dom bday → ( bday
‘𝐴) =
∅) |
34 | 32, 33 | sylnbir 331 |
. . . . 5
⊢ (¬
𝐴 ∈ No → ( bday
‘𝐴) =
∅) |
35 | 34 | fveq2d 6778 |
. . . 4
⊢ (¬
𝐴 ∈ No → ( O ‘( bday
‘𝐴)) = ( O
‘∅)) |
36 | | old0 34043 |
. . . 4
⊢ ( O
‘∅) = ∅ |
37 | 35, 36 | eqtrdi 2794 |
. . 3
⊢ (¬
𝐴 ∈ No → ( O ‘( bday
‘𝐴)) =
∅) |
38 | 19, 30, 37 | 3eqtr4a 2804 |
. 2
⊢ (¬
𝐴 ∈ No → (( L ‘𝐴) ∪ ( R ‘𝐴)) = ( O ‘( bday
‘𝐴))) |
39 | 18, 38 | pm2.61i 182 |
1
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) = ( O
‘( bday ‘𝐴)) |