Step | Hyp | Ref
| Expression |
1 | | elfvdm 6928 |
. . 3
β’ (π β ( M βπ΄) β π΄ β dom M ) |
2 | | madef 27359 |
. . . 4
β’ M
:OnβΆπ« No |
3 | 2 | fdmi 6729 |
. . 3
β’ dom M =
On |
4 | 1, 3 | eleqtrdi 2843 |
. 2
β’ (π β ( M βπ΄) β π΄ β On) |
5 | | fveq2 6891 |
. . . . . 6
β’ (π = π β ( M βπ) = ( M βπ)) |
6 | | sseq2 4008 |
. . . . . 6
β’ (π = π β (( bday
βπ₯) β
π β ( bday βπ₯) β π)) |
7 | 5, 6 | raleqbidv 3342 |
. . . . 5
β’ (π = π β (βπ₯ β ( M βπ)( bday
βπ₯) β
π β βπ₯ β ( M βπ)( bday
βπ₯) β
π)) |
8 | | fveq2 6891 |
. . . . . . 7
β’ (π₯ = π¦ β ( bday
βπ₯) = ( bday βπ¦)) |
9 | 8 | sseq1d 4013 |
. . . . . 6
β’ (π₯ = π¦ β (( bday
βπ₯) β
π β ( bday βπ¦) β π)) |
10 | 9 | cbvralvw 3234 |
. . . . 5
β’
(βπ₯ β (
M βπ)( bday βπ₯) β π β βπ¦ β ( M βπ)( bday
βπ¦) β
π) |
11 | 7, 10 | bitrdi 286 |
. . . 4
β’ (π = π β (βπ₯ β ( M βπ)( bday
βπ₯) β
π β βπ¦ β ( M βπ)( bday
βπ¦) β
π)) |
12 | | fveq2 6891 |
. . . . 5
β’ (π = π΄ β ( M βπ) = ( M βπ΄)) |
13 | | sseq2 4008 |
. . . . 5
β’ (π = π΄ β (( bday
βπ₯) β
π β ( bday βπ₯) β π΄)) |
14 | 12, 13 | raleqbidv 3342 |
. . . 4
β’ (π = π΄ β (βπ₯ β ( M βπ)( bday
βπ₯) β
π β βπ₯ β ( M βπ΄)( bday
βπ₯) β
π΄)) |
15 | | elmade2 27371 |
. . . . . . . 8
β’ (π β On β (π₯ β ( M βπ) β βπ β π« ( O
βπ)βπ β π« ( O
βπ)(π <<s π β§ (π |s π) = π₯))) |
16 | 15 | adantr 481 |
. . . . . . 7
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (π₯ β ( M βπ) β βπ β π« ( O
βπ)βπ β π« ( O
βπ)(π <<s π β§ (π |s π) = π₯))) |
17 | | elpwi 4609 |
. . . . . . . . . . 11
β’ (π β π« ( O
βπ) β π β ( O βπ)) |
18 | | elpwi 4609 |
. . . . . . . . . . 11
β’ (π β π« ( O
βπ) β π β ( O βπ)) |
19 | 17, 18 | anim12i 613 |
. . . . . . . . . 10
β’ ((π β π« ( O
βπ) β§ π β π« ( O
βπ)) β (π β ( O βπ) β§ π β ( O βπ))) |
20 | | unss 4184 |
. . . . . . . . . 10
β’ ((π β ( O βπ) β§ π β ( O βπ)) β (π βͺ π) β ( O βπ)) |
21 | 19, 20 | sylib 217 |
. . . . . . . . 9
β’ ((π β π« ( O
βπ) β§ π β π« ( O
βπ)) β (π βͺ π) β ( O βπ)) |
22 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β π <<s π) |
23 | | simplll 773 |
. . . . . . . . . . . . 13
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β π β On) |
24 | | dfss3 3970 |
. . . . . . . . . . . . . . . . 17
β’ ((π βͺ π) β ( O βπ) β βπ§ β (π βͺ π)π§ β ( O βπ)) |
25 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π§ β ( bday
βπ¦) = ( bday βπ§)) |
26 | 25 | sseq1d 4013 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ = π§ β (( bday
βπ¦) β
π β ( bday βπ§) β π)) |
27 | 26 | rspccv 3609 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(βπ¦ β (
M βπ)( bday βπ¦) β π β (π§ β ( M βπ) β ( bday
βπ§) β
π)) |
28 | 27 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π βπ¦ β ( M βπ)( bday
βπ¦) β
π β βπ β π (π§ β ( M βπ) β ( bday
βπ§) β
π)) |
29 | | rexim 3087 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
π (π§ β ( M βπ) β ( bday
βπ§) β
π) β (βπ β π π§ β ( M βπ) β βπ β π ( bday
βπ§) β
π)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ β
π βπ¦ β ( M βπ)( bday
βπ¦) β
π β (βπ β π π§ β ( M βπ) β βπ β π ( bday
βπ§) β
π)) |
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (βπ β π π§ β ( M βπ) β βπ β π ( bday
βπ§) β
π)) |
32 | | elold 27372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β On β (π§ β ( O βπ) β βπ β π π§ β ( M βπ))) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (π§ β ( O βπ) β βπ β π π§ β ( M βπ))) |
34 | | bdayelon 27285 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ( bday βπ§) β On |
35 | | onelssex 6412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((( bday βπ§) β On β§ π β On) β ((
bday βπ§)
β π β
βπ β π ( bday
βπ§) β
π)) |
36 | 34, 35 | mpan 688 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β On β (( bday βπ§) β π β βπ β π ( bday
βπ§) β
π)) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (( bday βπ§) β π β βπ β π ( bday
βπ§) β
π)) |
38 | 31, 33, 37 | 3imtr4d 293 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (π§ β ( O βπ) β (
bday βπ§)
β π)) |
39 | 38 | ralimdv 3169 |
. . . . . . . . . . . . . . . . 17
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (βπ§ β (π βͺ π)π§ β ( O βπ) β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
40 | 24, 39 | biimtrid 241 |
. . . . . . . . . . . . . . . 16
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β ((π βͺ π) β ( O βπ) β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
41 | 40 | imp 407 |
. . . . . . . . . . . . . . 15
β’ (((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β βπ§ β (π βͺ π)( bday
βπ§) β
π) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β βπ§ β (π βͺ π)( bday
βπ§) β
π) |
43 | | bdayfun 27281 |
. . . . . . . . . . . . . . . . 17
β’ Fun bday |
44 | | oldssno 27364 |
. . . . . . . . . . . . . . . . . . 19
β’ ( O
βπ) β No |
45 | | sstr 3990 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π βͺ π) β ( O βπ) β§ ( O βπ) β No )
β (π βͺ π) β
No ) |
46 | 44, 45 | mpan2 689 |
. . . . . . . . . . . . . . . . . 18
β’ ((π βͺ π) β ( O βπ) β (π βͺ π) β No
) |
47 | | bdaydm 27283 |
. . . . . . . . . . . . . . . . . 18
β’ dom bday = No
|
48 | 46, 47 | sseqtrrdi 4033 |
. . . . . . . . . . . . . . . . 17
β’ ((π βͺ π) β ( O βπ) β (π βͺ π) β dom bday
) |
49 | | funimass4 6956 |
. . . . . . . . . . . . . . . . 17
β’ ((Fun
bday β§ (π βͺ π) β dom bday
) β (( bday β (π βͺ π)) β π β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
50 | 43, 48, 49 | sylancr 587 |
. . . . . . . . . . . . . . . 16
β’ ((π βͺ π) β ( O βπ) β (( bday
β (π βͺ
π)) β π β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . 15
β’ (((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β (( bday
β (π βͺ
π)) β π β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β (( bday
β (π βͺ
π)) β π β βπ§ β (π βͺ π)( bday
βπ§) β
π)) |
53 | 42, 52 | mpbird 256 |
. . . . . . . . . . . . 13
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β ( bday
β (π βͺ π)) β π) |
54 | | scutbdaybnd 27324 |
. . . . . . . . . . . . 13
β’ ((π <<s π β§ π β On β§ ( bday
β (π βͺ
π)) β π) β (
bday β(π |s
π)) β π) |
55 | 22, 23, 53, 54 | syl3anc 1371 |
. . . . . . . . . . . 12
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β ( bday
β(π |s π)) β π) |
56 | | fveq2 6891 |
. . . . . . . . . . . . 13
β’ ((π |s π) = π₯ β ( bday
β(π |s π)) = (
bday βπ₯)) |
57 | 56 | sseq1d 4013 |
. . . . . . . . . . . 12
β’ ((π |s π) = π₯ β (( bday
β(π |s π)) β π β ( bday
βπ₯) β
π)) |
58 | 55, 57 | syl5ibcom 244 |
. . . . . . . . . . 11
β’ ((((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β§ π <<s π) β ((π |s π) = π₯ β ( bday
βπ₯) β
π)) |
59 | 58 | expimpd 454 |
. . . . . . . . . 10
β’ (((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β§ (π βͺ π) β ( O βπ)) β ((π <<s π β§ (π |s π) = π₯) β ( bday
βπ₯) β
π)) |
60 | 59 | ex 413 |
. . . . . . . . 9
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β ((π βͺ π) β ( O βπ) β ((π <<s π β§ (π |s π) = π₯) β ( bday
βπ₯) β
π))) |
61 | 21, 60 | syl5 34 |
. . . . . . . 8
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β ((π β π« ( O
βπ) β§ π β π« ( O
βπ)) β ((π <<s π β§ (π |s π) = π₯) β ( bday
βπ₯) β
π))) |
62 | 61 | rexlimdvv 3210 |
. . . . . . 7
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (βπ β π« ( O
βπ)βπ β π« ( O
βπ)(π <<s π β§ (π |s π) = π₯) β ( bday
βπ₯) β
π)) |
63 | 16, 62 | sylbid 239 |
. . . . . 6
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β (π₯ β ( M βπ) β (
bday βπ₯)
β π)) |
64 | 63 | ralrimiv 3145 |
. . . . 5
β’ ((π β On β§ βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π) β βπ₯ β ( M βπ)( bday
βπ₯) β
π) |
65 | 64 | ex 413 |
. . . 4
β’ (π β On β (βπ β π βπ¦ β ( M βπ)( bday
βπ¦) β
π β βπ₯ β ( M βπ)( bday
βπ₯) β
π)) |
66 | 11, 14, 65 | tfis3 7849 |
. . 3
β’ (π΄ β On β βπ₯ β ( M βπ΄)( bday
βπ₯) β
π΄) |
67 | | fveq2 6891 |
. . . . 5
β’ (π₯ = π β ( bday
βπ₯) = ( bday βπ)) |
68 | 67 | sseq1d 4013 |
. . . 4
β’ (π₯ = π β (( bday
βπ₯) β
π΄ β ( bday βπ) β π΄)) |
69 | 68 | rspccv 3609 |
. . 3
β’
(βπ₯ β (
M βπ΄)( bday βπ₯) β π΄ β (π β ( M βπ΄) β ( bday
βπ) β
π΄)) |
70 | 66, 69 | syl 17 |
. 2
β’ (π΄ β On β (π β ( M βπ΄) β (
bday βπ)
β π΄)) |
71 | 4, 70 | mpcom 38 |
1
β’ (π β ( M βπ΄) β (
bday βπ)
β π΄) |