Step | Hyp | Ref
| Expression |
1 | | cantnfs.a |
. . . . . 6
β’ (π β π΄ β On) |
2 | | cantnfs.b |
. . . . . . 7
β’ (π β π΅ β On) |
3 | | cantnfs.s |
. . . . . . . . 9
β’ π = dom (π΄ CNF π΅) |
4 | | oemapval.t |
. . . . . . . . 9
β’ π = {β¨π₯, π¦β© β£ βπ§ β π΅ ((π₯βπ§) β (π¦βπ§) β§ βπ€ β π΅ (π§ β π€ β (π₯βπ€) = (π¦βπ€)))} |
5 | | oemapval.f |
. . . . . . . . 9
β’ (π β πΉ β π) |
6 | | oemapval.g |
. . . . . . . . 9
β’ (π β πΊ β π) |
7 | | oemapvali.r |
. . . . . . . . 9
β’ (π β πΉππΊ) |
8 | | oemapvali.x |
. . . . . . . . 9
β’ π = βͺ
{π β π΅ β£ (πΉβπ) β (πΊβπ)} |
9 | 3, 1, 2, 4, 5, 6, 7, 8 | oemapvali 9628 |
. . . . . . . 8
β’ (π β (π β π΅ β§ (πΉβπ) β (πΊβπ) β§ βπ€ β π΅ (π β π€ β (πΉβπ€) = (πΊβπ€)))) |
10 | 9 | simp1d 1143 |
. . . . . . 7
β’ (π β π β π΅) |
11 | | onelon 6346 |
. . . . . . 7
β’ ((π΅ β On β§ π β π΅) β π β On) |
12 | 2, 10, 11 | syl2anc 585 |
. . . . . 6
β’ (π β π β On) |
13 | | oecl 8487 |
. . . . . 6
β’ ((π΄ β On β§ π β On) β (π΄ βo π) β On) |
14 | 1, 12, 13 | syl2anc 585 |
. . . . 5
β’ (π β (π΄ βo π) β On) |
15 | 3, 1, 2 | cantnfs 9610 |
. . . . . . . . 9
β’ (π β (πΊ β π β (πΊ:π΅βΆπ΄ β§ πΊ finSupp β
))) |
16 | 6, 15 | mpbid 231 |
. . . . . . . 8
β’ (π β (πΊ:π΅βΆπ΄ β§ πΊ finSupp β
)) |
17 | 16 | simpld 496 |
. . . . . . 7
β’ (π β πΊ:π΅βΆπ΄) |
18 | 17, 10 | ffvelcdmd 7040 |
. . . . . 6
β’ (π β (πΊβπ) β π΄) |
19 | | onelon 6346 |
. . . . . 6
β’ ((π΄ β On β§ (πΊβπ) β π΄) β (πΊβπ) β On) |
20 | 1, 18, 19 | syl2anc 585 |
. . . . 5
β’ (π β (πΊβπ) β On) |
21 | | omcl 8486 |
. . . . 5
β’ (((π΄ βo π) β On β§ (πΊβπ) β On) β ((π΄ βo π) Β·o (πΊβπ)) β On) |
22 | 14, 20, 21 | syl2anc 585 |
. . . 4
β’ (π β ((π΄ βo π) Β·o (πΊβπ)) β On) |
23 | | ovexd 7396 |
. . . . . . . . . 10
β’ (π β (πΊ supp β
) β V) |
24 | | cantnflem1.o |
. . . . . . . . . . . 12
β’ π = OrdIso( E , (πΊ supp β
)) |
25 | 3, 1, 2, 24, 6 | cantnfcl 9611 |
. . . . . . . . . . 11
β’ (π β ( E We (πΊ supp β
) β§ dom π β Ο)) |
26 | 25 | simpld 496 |
. . . . . . . . . 10
β’ (π β E We (πΊ supp β
)) |
27 | 24 | oiiso 9481 |
. . . . . . . . . 10
β’ (((πΊ supp β
) β V β§ E
We (πΊ supp β
)) β
π Isom E , E (dom π, (πΊ supp β
))) |
28 | 23, 26, 27 | syl2anc 585 |
. . . . . . . . 9
β’ (π β π Isom E , E (dom π, (πΊ supp β
))) |
29 | | isof1o 7272 |
. . . . . . . . 9
β’ (π Isom E , E (dom π, (πΊ supp β
)) β π:dom πβ1-1-ontoβ(πΊ supp β
)) |
30 | 28, 29 | syl 17 |
. . . . . . . 8
β’ (π β π:dom πβ1-1-ontoβ(πΊ supp β
)) |
31 | | f1ocnv 6800 |
. . . . . . . 8
β’ (π:dom πβ1-1-ontoβ(πΊ supp β
) β β‘π:(πΊ supp β
)β1-1-ontoβdom
π) |
32 | | f1of 6788 |
. . . . . . . 8
β’ (β‘π:(πΊ supp β
)β1-1-ontoβdom
π β β‘π:(πΊ supp β
)βΆdom π) |
33 | 30, 31, 32 | 3syl 18 |
. . . . . . 7
β’ (π β β‘π:(πΊ supp β
)βΆdom π) |
34 | 3, 1, 2, 4, 5, 6, 7, 8 | cantnflem1a 9629 |
. . . . . . 7
β’ (π β π β (πΊ supp β
)) |
35 | 33, 34 | ffvelcdmd 7040 |
. . . . . 6
β’ (π β (β‘πβπ) β dom π) |
36 | 25 | simprd 497 |
. . . . . 6
β’ (π β dom π β Ο) |
37 | | elnn 7817 |
. . . . . 6
β’ (((β‘πβπ) β dom π β§ dom π β Ο) β (β‘πβπ) β Ο) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . 5
β’ (π β (β‘πβπ) β Ο) |
39 | | cantnflem1.h |
. . . . . . 7
β’ π» = seqΟ((π β V, π§ β V β¦ (((π΄ βo (πβπ)) Β·o (πΊβ(πβπ))) +o π§)), β
) |
40 | 39 | cantnfvalf 9609 |
. . . . . 6
β’ π»:ΟβΆOn |
41 | 40 | ffvelcdmi 7038 |
. . . . 5
β’ ((β‘πβπ) β Ο β (π»β(β‘πβπ)) β On) |
42 | 38, 41 | syl 17 |
. . . 4
β’ (π β (π»β(β‘πβπ)) β On) |
43 | | oaword1 8503 |
. . . 4
β’ ((((π΄ βo π) Β·o (πΊβπ)) β On β§ (π»β(β‘πβπ)) β On) β ((π΄ βo π) Β·o (πΊβπ)) β (((π΄ βo π) Β·o (πΊβπ)) +o (π»β(β‘πβπ)))) |
44 | 22, 42, 43 | syl2anc 585 |
. . 3
β’ (π β ((π΄ βo π) Β·o (πΊβπ)) β (((π΄ βo π) Β·o (πΊβπ)) +o (π»β(β‘πβπ)))) |
45 | 3, 1, 2, 24, 6, 39 | cantnfsuc 9614 |
. . . . 5
β’ ((π β§ (β‘πβπ) β Ο) β (π»βsuc (β‘πβπ)) = (((π΄ βo (πβ(β‘πβπ))) Β·o (πΊβ(πβ(β‘πβπ)))) +o (π»β(β‘πβπ)))) |
46 | 38, 45 | mpdan 686 |
. . . 4
β’ (π β (π»βsuc (β‘πβπ)) = (((π΄ βo (πβ(β‘πβπ))) Β·o (πΊβ(πβ(β‘πβπ)))) +o (π»β(β‘πβπ)))) |
47 | | f1ocnvfv2 7227 |
. . . . . . . 8
β’ ((π:dom πβ1-1-ontoβ(πΊ supp β
) β§ π β (πΊ supp β
)) β (πβ(β‘πβπ)) = π) |
48 | 30, 34, 47 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ(β‘πβπ)) = π) |
49 | 48 | oveq2d 7377 |
. . . . . 6
β’ (π β (π΄ βo (πβ(β‘πβπ))) = (π΄ βo π)) |
50 | 48 | fveq2d 6850 |
. . . . . 6
β’ (π β (πΊβ(πβ(β‘πβπ))) = (πΊβπ)) |
51 | 49, 50 | oveq12d 7379 |
. . . . 5
β’ (π β ((π΄ βo (πβ(β‘πβπ))) Β·o (πΊβ(πβ(β‘πβπ)))) = ((π΄ βo π) Β·o (πΊβπ))) |
52 | 51 | oveq1d 7376 |
. . . 4
β’ (π β (((π΄ βo (πβ(β‘πβπ))) Β·o (πΊβ(πβ(β‘πβπ)))) +o (π»β(β‘πβπ))) = (((π΄ βo π) Β·o (πΊβπ)) +o (π»β(β‘πβπ)))) |
53 | 46, 52 | eqtrd 2773 |
. . 3
β’ (π β (π»βsuc (β‘πβπ)) = (((π΄ βo π) Β·o (πΊβπ)) +o (π»β(β‘πβπ)))) |
54 | 44, 53 | sseqtrrd 3989 |
. 2
β’ (π β ((π΄ βo π) Β·o (πΊβπ)) β (π»βsuc (β‘πβπ))) |
55 | | onss 7723 |
. . . . . . . . . . 11
β’ (π΅ β On β π΅ β On) |
56 | 2, 55 | syl 17 |
. . . . . . . . . 10
β’ (π β π΅ β On) |
57 | 56 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β π₯ β On) |
58 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΅) β π β On) |
59 | | onsseleq 6362 |
. . . . . . . . 9
β’ ((π₯ β On β§ π β On) β (π₯ β π β (π₯ β π β¨ π₯ = π))) |
60 | 57, 58, 59 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β π΅) β (π₯ β π β (π₯ β π β¨ π₯ = π))) |
61 | | orcom 869 |
. . . . . . . 8
β’ ((π₯ β π β¨ π₯ = π) β (π₯ = π β¨ π₯ β π)) |
62 | 60, 61 | bitrdi 287 |
. . . . . . 7
β’ ((π β§ π₯ β π΅) β (π₯ β π β (π₯ = π β¨ π₯ β π))) |
63 | 62 | ifbid 4513 |
. . . . . 6
β’ ((π β§ π₯ β π΅) β if(π₯ β π, (πΉβπ₯), β
) = if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
)) |
64 | 63 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π₯ β π΅ β¦ if(π₯ β π, (πΉβπ₯), β
)) = (π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
))) |
65 | 64 | fveq2d 6850 |
. . . 4
β’ (π β ((π΄ CNF π΅)β(π₯ β π΅ β¦ if(π₯ β π, (πΉβπ₯), β
))) = ((π΄ CNF π΅)β(π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
)))) |
66 | 3, 1, 2 | cantnfs 9610 |
. . . . . . . . . . . 12
β’ (π β (πΉ β π β (πΉ:π΅βΆπ΄ β§ πΉ finSupp β
))) |
67 | 5, 66 | mpbid 231 |
. . . . . . . . . . 11
β’ (π β (πΉ:π΅βΆπ΄ β§ πΉ finSupp β
)) |
68 | 67 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΉ:π΅βΆπ΄) |
69 | 68 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΅) β (πΉβπ¦) β π΄) |
70 | 18 | ne0d 4299 |
. . . . . . . . . . 11
β’ (π β π΄ β β
) |
71 | | on0eln0 6377 |
. . . . . . . . . . . 12
β’ (π΄ β On β (β
β π΄ β π΄ β β
)) |
72 | 1, 71 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β
β π΄ β π΄ β β
)) |
73 | 70, 72 | mpbird 257 |
. . . . . . . . . 10
β’ (π β β
β π΄) |
74 | 73 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β π΅) β β
β π΄) |
75 | 69, 74 | ifcld 4536 |
. . . . . . . 8
β’ ((π β§ π¦ β π΅) β if(π¦ β π, (πΉβπ¦), β
) β π΄) |
76 | 75 | fmpttd 7067 |
. . . . . . 7
β’ (π β (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)):π΅βΆπ΄) |
77 | | 0ex 5268 |
. . . . . . . . 9
β’ β
β V |
78 | 77 | a1i 11 |
. . . . . . . 8
β’ (π β β
β
V) |
79 | 67 | simprd 497 |
. . . . . . . 8
β’ (π β πΉ finSupp β
) |
80 | 68, 2, 78, 79 | fsuppmptif 9343 |
. . . . . . 7
β’ (π β (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) finSupp
β
) |
81 | 3, 1, 2 | cantnfs 9610 |
. . . . . . 7
β’ (π β ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) β π β ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)):π΅βΆπ΄ β§ (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) finSupp
β
))) |
82 | 76, 80, 81 | mpbir2and 712 |
. . . . . 6
β’ (π β (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) β π) |
83 | 68, 10 | ffvelcdmd 7040 |
. . . . . 6
β’ (π β (πΉβπ) β π΄) |
84 | | eldifn 4091 |
. . . . . . . . 9
β’ (π¦ β (π΅ β π) β Β¬ π¦ β π) |
85 | 84 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π¦ β (π΅ β π)) β Β¬ π¦ β π) |
86 | 85 | iffalsed 4501 |
. . . . . . 7
β’ ((π β§ π¦ β (π΅ β π)) β if(π¦ β π, (πΉβπ¦), β
) = β
) |
87 | 86, 2 | suppss2 8135 |
. . . . . 6
β’ (π β ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) supp β
) β π) |
88 | | ifor 4544 |
. . . . . . . 8
β’ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
) = if(π₯ = π, (πΉβπ₯), if(π₯ β π, (πΉβπ₯), β
)) |
89 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π₯ = π β (πΉβπ₯) = (πΉβπ)) |
90 | 89 | adantl 483 |
. . . . . . . . . 10
β’ ((π₯ β π΅ β§ π₯ = π) β (πΉβπ₯) = (πΉβπ)) |
91 | 90 | ifeq1da 4521 |
. . . . . . . . 9
β’ (π₯ β π΅ β if(π₯ = π, (πΉβπ₯), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯)) = if(π₯ = π, (πΉβπ), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯))) |
92 | | eleq1w 2817 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (π¦ β π β π₯ β π)) |
93 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
94 | 92, 93 | ifbieq1d 4514 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β if(π¦ β π, (πΉβπ¦), β
) = if(π₯ β π, (πΉβπ₯), β
)) |
95 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) = (π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)) |
96 | | fvex 6859 |
. . . . . . . . . . . 12
β’ (πΉβπ₯) β V |
97 | 96, 77 | ifex 4540 |
. . . . . . . . . . 11
β’ if(π₯ β π, (πΉβπ₯), β
) β V |
98 | 94, 95, 97 | fvmpt 6952 |
. . . . . . . . . 10
β’ (π₯ β π΅ β ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯) = if(π₯ β π, (πΉβπ₯), β
)) |
99 | 98 | ifeq2d 4510 |
. . . . . . . . 9
β’ (π₯ β π΅ β if(π₯ = π, (πΉβπ₯), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯)) = if(π₯ = π, (πΉβπ₯), if(π₯ β π, (πΉβπ₯), β
))) |
100 | 91, 99 | eqtr3d 2775 |
. . . . . . . 8
β’ (π₯ β π΅ β if(π₯ = π, (πΉβπ), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯)) = if(π₯ = π, (πΉβπ₯), if(π₯ β π, (πΉβπ₯), β
))) |
101 | 88, 100 | eqtr4id 2792 |
. . . . . . 7
β’ (π₯ β π΅ β if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
) = if(π₯ = π, (πΉβπ), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯))) |
102 | 101 | mpteq2ia 5212 |
. . . . . 6
β’ (π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
)) = (π₯ β π΅ β¦ if(π₯ = π, (πΉβπ), ((π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))βπ₯))) |
103 | 3, 1, 2, 82, 10, 83, 87, 102 | cantnfp1 9625 |
. . . . 5
β’ (π β ((π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
)) β π β§ ((π΄ CNF π΅)β(π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
))) = (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)))))) |
104 | 103 | simprd 497 |
. . . 4
β’ (π β ((π΄ CNF π΅)β(π₯ β π΅ β¦ if((π₯ = π β¨ π₯ β π), (πΉβπ₯), β
))) = (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))))) |
105 | 65, 104 | eqtrd 2773 |
. . 3
β’ (π β ((π΄ CNF π΅)β(π₯ β π΅ β¦ if(π₯ β π, (πΉβπ₯), β
))) = (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))))) |
106 | | onelon 6346 |
. . . . . . 7
β’ ((π΄ β On β§ (πΉβπ) β π΄) β (πΉβπ) β On) |
107 | 1, 83, 106 | syl2anc 585 |
. . . . . 6
β’ (π β (πΉβπ) β On) |
108 | | omsuc 8476 |
. . . . . 6
β’ (((π΄ βo π) β On β§ (πΉβπ) β On) β ((π΄ βo π) Β·o suc (πΉβπ)) = (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π))) |
109 | 14, 107, 108 | syl2anc 585 |
. . . . 5
β’ (π β ((π΄ βo π) Β·o suc (πΉβπ)) = (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π))) |
110 | | eloni 6331 |
. . . . . . . 8
β’ ((πΊβπ) β On β Ord (πΊβπ)) |
111 | 20, 110 | syl 17 |
. . . . . . 7
β’ (π β Ord (πΊβπ)) |
112 | 9 | simp2d 1144 |
. . . . . . 7
β’ (π β (πΉβπ) β (πΊβπ)) |
113 | | ordsucss 7757 |
. . . . . . 7
β’ (Ord
(πΊβπ) β ((πΉβπ) β (πΊβπ) β suc (πΉβπ) β (πΊβπ))) |
114 | 111, 112,
113 | sylc 65 |
. . . . . 6
β’ (π β suc (πΉβπ) β (πΊβπ)) |
115 | | onsuc 7750 |
. . . . . . . 8
β’ ((πΉβπ) β On β suc (πΉβπ) β On) |
116 | 107, 115 | syl 17 |
. . . . . . 7
β’ (π β suc (πΉβπ) β On) |
117 | | omwordi 8522 |
. . . . . . 7
β’ ((suc
(πΉβπ) β On β§ (πΊβπ) β On β§ (π΄ βo π) β On) β (suc (πΉβπ) β (πΊβπ) β ((π΄ βo π) Β·o suc (πΉβπ)) β ((π΄ βo π) Β·o (πΊβπ)))) |
118 | 116, 20, 14, 117 | syl3anc 1372 |
. . . . . 6
β’ (π β (suc (πΉβπ) β (πΊβπ) β ((π΄ βo π) Β·o suc (πΉβπ)) β ((π΄ βo π) Β·o (πΊβπ)))) |
119 | 114, 118 | mpd 15 |
. . . . 5
β’ (π β ((π΄ βo π) Β·o suc (πΉβπ)) β ((π΄ βo π) Β·o (πΊβπ))) |
120 | 109, 119 | eqsstrrd 3987 |
. . . 4
β’ (π β (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π)) β ((π΄ βo π) Β·o (πΊβπ))) |
121 | 3, 1, 2, 82, 73, 12, 87 | cantnflt2 9617 |
. . . . 5
β’ (π β ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β (π΄ βo π)) |
122 | | onelon 6346 |
. . . . . . 7
β’ (((π΄ βo π) β On β§ ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β (π΄ βo π)) β ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β On) |
123 | 14, 121, 122 | syl2anc 585 |
. . . . . 6
β’ (π β ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β On) |
124 | | omcl 8486 |
. . . . . . 7
β’ (((π΄ βo π) β On β§ (πΉβπ) β On) β ((π΄ βo π) Β·o (πΉβπ)) β On) |
125 | 14, 107, 124 | syl2anc 585 |
. . . . . 6
β’ (π β ((π΄ βo π) Β·o (πΉβπ)) β On) |
126 | | oaord 8498 |
. . . . . 6
β’ ((((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β On β§ (π΄ βo π) β On β§ ((π΄ βo π) Β·o (πΉβπ)) β On) β (((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β (π΄ βo π) β (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)))) β (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π)))) |
127 | 123, 14, 125, 126 | syl3anc 1372 |
. . . . 5
β’ (π β (((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
))) β (π΄ βo π) β (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)))) β (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π)))) |
128 | 121, 127 | mpbid 231 |
. . . 4
β’ (π β (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)))) β (((π΄ βo π) Β·o (πΉβπ)) +o (π΄ βo π))) |
129 | 120, 128 | sseldd 3949 |
. . 3
β’ (π β (((π΄ βo π) Β·o (πΉβπ)) +o ((π΄ CNF π΅)β(π¦ β π΅ β¦ if(π¦ β π, (πΉβπ¦), β
)))) β ((π΄ βo π) Β·o (πΊβπ))) |
130 | 105, 129 | eqeltrd 2834 |
. 2
β’ (π β ((π΄ CNF π΅)β(π₯ β π΅ β¦ if(π₯ β π, (πΉβπ₯), β
))) β ((π΄ βo π) Β·o (πΊβπ))) |
131 | 54, 130 | sseldd 3949 |
1
β’ (π β ((π΄ CNF π΅)β(π₯ β π΅ β¦ if(π₯ β π, (πΉβπ₯), β
))) β (π»βsuc (β‘πβπ))) |