Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . 4
โข {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} = {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} |
2 | | cantnfs.a |
. . . 4
โข (๐ โ ๐ด โ On) |
3 | | cantnfs.b |
. . . 4
โข (๐ โ ๐ต โ On) |
4 | 1, 2, 3 | cantnffval 9607 |
. . 3
โข (๐ โ (๐ด CNF ๐ต) = (๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |
5 | 4 | fveq1d 6848 |
. 2
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = ((๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))โ๐น)) |
6 | | cantnfcl.f |
. . . 4
โข (๐ โ ๐น โ ๐) |
7 | | cantnfs.s |
. . . . 5
โข ๐ = dom (๐ด CNF ๐ต) |
8 | 1, 2, 3 | cantnfdm 9608 |
. . . . 5
โข (๐ โ dom (๐ด CNF ๐ต) = {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
}) |
9 | 7, 8 | eqtrid 2785 |
. . . 4
โข (๐ โ ๐ = {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
}) |
10 | 6, 9 | eleqtrd 2836 |
. . 3
โข (๐ โ ๐น โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
}) |
11 | | ovex 7394 |
. . . . . 6
โข (๐ supp โ
) โ
V |
12 | | eqid 2733 |
. . . . . . 7
โข OrdIso( E
, (๐ supp โ
)) =
OrdIso( E , (๐ supp
โ
)) |
13 | 12 | oiexg 9479 |
. . . . . 6
โข ((๐ supp โ
) โ V โ
OrdIso( E , (๐ supp
โ
)) โ V) |
14 | 11, 13 | mp1i 13 |
. . . . 5
โข (๐ = ๐น โ OrdIso( E , (๐ supp โ
)) โ V) |
15 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ โ = OrdIso( E , (๐ supp โ
))) |
16 | | oveq1 7368 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐น โ (๐ supp โ
) = (๐น supp โ
)) |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (๐ supp โ
) = (๐น supp โ
)) |
18 | | oieq2 9457 |
. . . . . . . . . . . . . . . 16
โข ((๐ supp โ
) = (๐น supp โ
) โ OrdIso( E
, (๐ supp โ
)) =
OrdIso( E , (๐น supp
โ
))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ OrdIso( E , (๐ supp โ
)) = OrdIso( E ,
(๐น supp
โ
))) |
20 | 15, 19 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ โ = OrdIso( E , (๐น supp โ
))) |
21 | | cantnfcl.g |
. . . . . . . . . . . . . 14
โข ๐บ = OrdIso( E , (๐น supp โ
)) |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . . . . . . 13
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ โ = ๐บ) |
23 | 22 | fveq1d 6848 |
. . . . . . . . . . . 12
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (โโ๐) = (๐บโ๐)) |
24 | 23 | oveq2d 7377 |
. . . . . . . . . . 11
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (๐ด โo (โโ๐)) = (๐ด โo (๐บโ๐))) |
25 | | simpl 484 |
. . . . . . . . . . . 12
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ ๐ = ๐น) |
26 | 25, 23 | fveq12d 6853 |
. . . . . . . . . . 11
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (๐โ(โโ๐)) = (๐นโ(๐บโ๐))) |
27 | 24, 26 | oveq12d 7379 |
. . . . . . . . . 10
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ ((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) = ((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐)))) |
28 | 27 | oveq1d 7376 |
. . . . . . . . 9
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง) = (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) |
29 | 28 | mpoeq3dv 7440 |
. . . . . . . 8
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ (๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))) |
30 | | eqid 2733 |
. . . . . . . 8
โข โ
=
โ
|
31 | | seqomeq12 8404 |
. . . . . . . 8
โข (((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) โง โ
= โ
) โ
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
)) |
32 | 29, 30, 31 | sylancl 587 |
. . . . . . 7
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
)) |
33 | | cantnfval.h |
. . . . . . 7
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
34 | 32, 33 | eqtr4di 2791 |
. . . . . 6
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) = ๐ป) |
35 | 22 | dmeqd 5865 |
. . . . . 6
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ dom โ = dom ๐บ) |
36 | 34, 35 | fveq12d 6853 |
. . . . 5
โข ((๐ = ๐น โง โ = OrdIso( E , (๐ supp โ
))) โ
(seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ด
โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) = (๐ปโdom ๐บ)) |
37 | 14, 36 | csbied 3897 |
. . . 4
โข (๐ = ๐น โ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) = (๐ปโdom ๐บ)) |
38 | | eqid 2733 |
. . . 4
โข (๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) = (๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) |
39 | | fvex 6859 |
. . . 4
โข (๐ปโdom ๐บ) โ V |
40 | 37, 38, 39 | fvmpt 6952 |
. . 3
โข (๐น โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โ ((๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))โ๐น) = (๐ปโdom ๐บ)) |
41 | 10, 40 | syl 17 |
. 2
โข (๐ โ ((๐ โ {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))โ๐น) = (๐ปโdom ๐บ)) |
42 | 5, 41 | eqtrd 2773 |
1
โข (๐ โ ((๐ด CNF ๐ต)โ๐น) = (๐ปโdom ๐บ)) |