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