Step | Hyp | Ref
| Expression |
1 | | noinfbday.1 |
. . . . 5
β’ π = if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) |
2 | 1 | noinfno 27082 |
. . . 4
β’ ((π΅ β
No β§ π΅ β
π) β π β No
) |
3 | | bdayval 27012 |
. . . 4
β’ (π β
No β ( bday βπ) = dom π) |
4 | 2, 3 | syl 17 |
. . 3
β’ ((π΅ β
No β§ π΅ β
π) β ( bday βπ) = dom π) |
5 | 4 | adantr 482 |
. 2
β’ (((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β ( bday βπ) = dom π) |
6 | | iftrue 4493 |
. . . . . . . 8
β’
(βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β if(βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯, ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}), (π β {π¦ β£ βπ’ β π΅ (π¦ β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π¦) = (π£ βΎ suc π¦)))} β¦ (β©π₯βπ’ β π΅ (π β dom π’ β§ βπ£ β π΅ (Β¬ π’ <s π£ β (π’ βΎ suc π) = (π£ βΎ suc π)) β§ (π’βπ) = π₯)))) = ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©})) |
7 | 1, 6 | eqtrid 2785 |
. . . . . . 7
β’
(βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β π = ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©})) |
8 | 7 | dmeqd 5862 |
. . . . . 6
β’
(βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β dom π = dom ((β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©})) |
9 | | 1oex 8423 |
. . . . . . . . 9
β’
1o β V |
10 | 9 | dmsnop 6169 |
. . . . . . . 8
β’ dom
{β¨dom (β©π₯
β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©} = {dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)} |
11 | 10 | uneq2i 4121 |
. . . . . . 7
β’ (dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ dom {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}) = (dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)}) |
12 | | dmun 5867 |
. . . . . . 7
β’ dom
((β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}) = (dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ dom {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}) |
13 | | df-suc 6324 |
. . . . . . 7
β’ suc dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) = (dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)}) |
14 | 11, 12, 13 | 3eqtr4i 2771 |
. . . . . 6
β’ dom
((β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) βͺ {β¨dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯), 1oβ©}) = suc dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) |
15 | 8, 14 | eqtrdi 2789 |
. . . . 5
β’
(βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β dom π = suc dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) |
16 | 15 | adantr 482 |
. . . 4
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β dom
π = suc dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) |
17 | | simprrl 780 |
. . . . . 6
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β π β On) |
18 | | eloni 6328 |
. . . . . 6
β’ (π β On β Ord π) |
19 | 17, 18 | syl 17 |
. . . . 5
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β Ord
π) |
20 | | simprll 778 |
. . . . . . . 8
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β π΅ β
No ) |
21 | | simpl 484 |
. . . . . . . . . 10
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β
βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) |
22 | | nominmo 27063 |
. . . . . . . . . . 11
β’ (π΅ β
No β β*π₯
β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) |
23 | 20, 22 | syl 17 |
. . . . . . . . . 10
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β
β*π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) |
24 | | reu5 3354 |
. . . . . . . . . 10
β’
(β!π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β (βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ β*π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) |
25 | 21, 23, 24 | sylanbrc 584 |
. . . . . . . . 9
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β
β!π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) |
26 | | riotacl 7332 |
. . . . . . . . 9
β’
(β!π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π΅) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π΅) |
28 | 20, 27 | sseldd 3946 |
. . . . . . 7
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β No
) |
29 | | bdayval 27012 |
. . . . . . 7
β’
((β©π₯
β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β No
β ( bday β(β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) = dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) |
30 | 28, 29 | syl 17 |
. . . . . 6
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β ( bday β(β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) = dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) |
31 | | simprrr 781 |
. . . . . . 7
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β ( bday β π΅) β π) |
32 | | bdayfo 27041 |
. . . . . . . . 9
β’ bday : No βontoβOn |
33 | | fofn 6759 |
. . . . . . . . 9
β’ ( bday : No βontoβOn β bday
Fn No ) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
β’ bday Fn No
|
35 | | fnfvima 7184 |
. . . . . . . 8
β’ (( bday Fn No β§ π΅ β
No β§ (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π΅) β ( bday
β(β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) β ( bday
β π΅)) |
36 | 34, 20, 27, 35 | mp3an2i 1467 |
. . . . . . 7
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β ( bday β(β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) β ( bday
β π΅)) |
37 | 31, 36 | sseldd 3946 |
. . . . . 6
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β ( bday β(β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯)) β π) |
38 | 30, 37 | eqeltrrd 2835 |
. . . . 5
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π) |
39 | | ordsucss 7754 |
. . . . 5
β’ (Ord
π β (dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π β suc dom (β©π₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π)) |
40 | 19, 38, 39 | sylc 65 |
. . . 4
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β suc dom
(β©π₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯) β π) |
41 | 16, 40 | eqsstrd 3983 |
. . 3
β’
((βπ₯ β
π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β dom
π β π) |
42 | 1 | noinfdm 27083 |
. . . . 5
β’ (Β¬
βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β dom π = {π§ β£ βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))}) |
43 | 42 | adantr 482 |
. . . 4
β’ ((Β¬
βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β dom
π = {π§ β£ βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))}) |
44 | | simplrl 776 |
. . . . . . . . . . 11
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β π β On) |
45 | 44, 18 | syl 17 |
. . . . . . . . . 10
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β Ord π) |
46 | | ssel2 3940 |
. . . . . . . . . . . . 13
β’ ((π΅ β
No β§ π β
π΅) β π β
No ) |
47 | 46 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β π β No
) |
48 | | bdayval 27012 |
. . . . . . . . . . . 12
β’ (π β
No β ( bday βπ) = dom π) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β ( bday
βπ) = dom
π) |
50 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β ( bday
β π΅) β
π) |
51 | | fnfvima 7184 |
. . . . . . . . . . . . . 14
β’ (( bday Fn No β§ π΅ β
No β§ π β
π΅) β ( bday βπ) β ( bday
β π΅)) |
52 | 34, 51 | mp3an1 1449 |
. . . . . . . . . . . . 13
β’ ((π΅ β
No β§ π β
π΅) β ( bday βπ) β ( bday
β π΅)) |
53 | 52 | ad4ant14 751 |
. . . . . . . . . . . 12
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β ( bday
βπ) β
( bday β π΅)) |
54 | 50, 53 | sseldd 3946 |
. . . . . . . . . . 11
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β ( bday
βπ) β
π) |
55 | 49, 54 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β dom π β π) |
56 | | ordelss 6334 |
. . . . . . . . . 10
β’ ((Ord
π β§ dom π β π) β dom π β π) |
57 | 45, 55, 56 | syl2anc 585 |
. . . . . . . . 9
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β dom π β π) |
58 | 57 | sseld 3944 |
. . . . . . . 8
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β (π§ β dom π β π§ β π)) |
59 | 58 | adantrd 493 |
. . . . . . 7
β’ ((((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β§ π β π΅) β ((π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§))) β π§ β π)) |
60 | 59 | rexlimdva 3149 |
. . . . . 6
β’ (((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β
(βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§))) β π§ β π)) |
61 | 60 | abssdv 4026 |
. . . . 5
β’ (((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β {π§ β£ βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))} β π) |
62 | 61 | adantl 483 |
. . . 4
β’ ((Β¬
βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β {π§ β£ βπ β π΅ (π§ β dom π β§ βπ β π΅ (Β¬ π <s π β (π βΎ suc π§) = (π βΎ suc π§)))} β π) |
63 | 43, 62 | eqsstrd 3983 |
. . 3
β’ ((Β¬
βπ₯ β π΅ βπ¦ β π΅ Β¬ π¦ <s π₯ β§ ((π΅ β No
β§ π΅ β π) β§ (π β On β§ (
bday β π΅)
β π))) β dom
π β π) |
64 | 41, 63 | pm2.61ian 811 |
. 2
β’ (((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β dom
π β π) |
65 | 5, 64 | eqsstrd 3983 |
1
β’ (((π΅ β
No β§ π΅ β
π) β§ (π β On β§ (
bday β π΅)
β π)) β ( bday βπ) β π) |