Step | Hyp | Ref
| Expression |
1 | | leftval 27358 |
. . . . 5
β’ ( L
βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π₯ <s π΄} |
2 | | rightval 27359 |
. . . . 5
β’ ( R
βπ΄) = {π₯ β ( O β( bday βπ΄)) β£ π΄ <s π₯} |
3 | 1, 2 | uneq12i 4162 |
. . . 4
β’ (( L
βπ΄) βͺ ( R
βπ΄)) = ({π₯ β ( O β( bday βπ΄)) β£ π₯ <s π΄} βͺ {π₯ β ( O β(
bday βπ΄))
β£ π΄ <s π₯}) |
4 | | unrab 4306 |
. . . 4
β’ ({π₯ β ( O β( bday βπ΄)) β£ π₯ <s π΄} βͺ {π₯ β ( O β(
bday βπ΄))
β£ π΄ <s π₯}) = {π₯ β ( O β(
bday βπ΄))
β£ (π₯ <s π΄ β¨ π΄ <s π₯)} |
5 | 3, 4 | eqtri 2761 |
. . 3
β’ (( L
βπ΄) βͺ ( R
βπ΄)) = {π₯ β ( O β( bday βπ΄)) β£ (π₯ <s π΄ β¨ π΄ <s π₯)} |
6 | | oldirr 27384 |
. . . . . . . 8
β’ Β¬
π΄ β ( O β( bday βπ΄)) |
7 | | eleq1 2822 |
. . . . . . . 8
β’ (π₯ = π΄ β (π₯ β ( O β(
bday βπ΄))
β π΄ β ( O
β( bday βπ΄)))) |
8 | 6, 7 | mtbiri 327 |
. . . . . . 7
β’ (π₯ = π΄ β Β¬ π₯ β ( O β(
bday βπ΄))) |
9 | 8 | necon2ai 2971 |
. . . . . 6
β’ (π₯ β ( O β( bday βπ΄)) β π₯ β π΄) |
10 | 9 | adantl 483 |
. . . . 5
β’ ((π΄ β
No β§ π₯ β (
O β( bday βπ΄))) β π₯ β π΄) |
11 | | oldssno 27356 |
. . . . . . 7
β’ ( O
β( bday βπ΄)) β No
|
12 | 11 | sseli 3979 |
. . . . . 6
β’ (π₯ β ( O β( bday βπ΄)) β π₯ β No
) |
13 | | slttrine 27254 |
. . . . . . 7
β’ ((π₯ β
No β§ π΄ β
No ) β (π₯ β π΄ β (π₯ <s π΄ β¨ π΄ <s π₯))) |
14 | 13 | ancoms 460 |
. . . . . 6
β’ ((π΄ β
No β§ π₯ β
No ) β (π₯ β π΄ β (π₯ <s π΄ β¨ π΄ <s π₯))) |
15 | 12, 14 | sylan2 594 |
. . . . 5
β’ ((π΄ β
No β§ π₯ β (
O β( bday βπ΄))) β (π₯ β π΄ β (π₯ <s π΄ β¨ π΄ <s π₯))) |
16 | 10, 15 | mpbid 231 |
. . . 4
β’ ((π΄ β
No β§ π₯ β (
O β( bday βπ΄))) β (π₯ <s π΄ β¨ π΄ <s π₯)) |
17 | 16 | rabeqcda 3444 |
. . 3
β’ (π΄ β
No β {π₯ β
( O β( bday βπ΄)) β£ (π₯ <s π΄ β¨ π΄ <s π₯)} = ( O β( bday
βπ΄))) |
18 | 5, 17 | eqtrid 2785 |
. 2
β’ (π΄ β
No β (( L βπ΄) βͺ ( R βπ΄)) = ( O β( bday
βπ΄))) |
19 | | un0 4391 |
. . 3
β’ (β
βͺ β
) = β
|
20 | | leftf 27360 |
. . . . . . 7
β’ L : No βΆπ« No
|
21 | 20 | fdmi 6730 |
. . . . . 6
β’ dom L =
No |
22 | 21 | eleq2i 2826 |
. . . . 5
β’ (π΄ β dom L β π΄ β
No ) |
23 | | ndmfv 6927 |
. . . . 5
β’ (Β¬
π΄ β dom L β ( L
βπ΄) =
β
) |
24 | 22, 23 | sylnbir 331 |
. . . 4
β’ (Β¬
π΄ β No β ( L βπ΄) = β
) |
25 | | rightf 27361 |
. . . . . . 7
β’ R : No βΆπ« No
|
26 | 25 | fdmi 6730 |
. . . . . 6
β’ dom R =
No |
27 | 26 | eleq2i 2826 |
. . . . 5
β’ (π΄ β dom R β π΄ β
No ) |
28 | | ndmfv 6927 |
. . . . 5
β’ (Β¬
π΄ β dom R β ( R
βπ΄) =
β
) |
29 | 27, 28 | sylnbir 331 |
. . . 4
β’ (Β¬
π΄ β No β ( R βπ΄) = β
) |
30 | 24, 29 | uneq12d 4165 |
. . 3
β’ (Β¬
π΄ β No β (( L βπ΄) βͺ ( R βπ΄)) = (β
βͺ
β
)) |
31 | | bdaydm 27276 |
. . . . . . 7
β’ dom bday = No
|
32 | 31 | eleq2i 2826 |
. . . . . 6
β’ (π΄ β dom bday β π΄ β No
) |
33 | | ndmfv 6927 |
. . . . . 6
β’ (Β¬
π΄ β dom bday β ( bday
βπ΄) =
β
) |
34 | 32, 33 | sylnbir 331 |
. . . . 5
β’ (Β¬
π΄ β No β ( bday
βπ΄) =
β
) |
35 | 34 | fveq2d 6896 |
. . . 4
β’ (Β¬
π΄ β No β ( O β( bday
βπ΄)) = ( O
ββ
)) |
36 | | old0 27354 |
. . . 4
β’ ( O
ββ
) = β
|
37 | 35, 36 | eqtrdi 2789 |
. . 3
β’ (Β¬
π΄ β No β ( O β( bday
βπ΄)) =
β
) |
38 | 19, 30, 37 | 3eqtr4a 2799 |
. 2
β’ (Β¬
π΄ β No β (( L βπ΄) βͺ ( R βπ΄)) = ( O β( bday
βπ΄))) |
39 | 18, 38 | pm2.61i 182 |
1
β’ (( L
βπ΄) βͺ ( R
βπ΄)) = ( O
β( bday βπ΄)) |