Step | Hyp | Ref
| Expression |
1 | | cantnffval.a |
. 2
โข (๐ โ ๐ด โ On) |
2 | | cantnffval.b |
. 2
โข (๐ โ ๐ต โ On) |
3 | | oveq12 7312 |
. . . . . 6
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ (๐ฅ โm ๐ฆ) = (๐ด โm ๐ต)) |
4 | 3 | rabeqdv 3426 |
. . . . 5
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} = {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
}) |
5 | | cantnffval.s |
. . . . 5
โข ๐ = {๐ โ (๐ด โm ๐ต) โฃ ๐ finSupp โ
} |
6 | 4, 5 | eqtr4di 2794 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} = ๐) |
7 | | simp1l 1197 |
. . . . . . . . . . 11
โข (((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โง ๐ โ V โง ๐ง โ V) โ ๐ฅ = ๐ด) |
8 | 7 | oveq1d 7318 |
. . . . . . . . . 10
โข (((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โง ๐ โ V โง ๐ง โ V) โ (๐ฅ โo (โโ๐)) = (๐ด โo (โโ๐))) |
9 | 8 | oveq1d 7318 |
. . . . . . . . 9
โข (((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โง ๐ โ V โง ๐ง โ V) โ ((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) = ((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐)))) |
10 | 9 | oveq1d 7318 |
. . . . . . . 8
โข (((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โง ๐ โ V โง ๐ง โ V) โ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง) = (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) |
11 | 10 | mpoeq3dva 7380 |
. . . . . . 7
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ (๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง))) |
12 | | eqid 2736 |
. . . . . . 7
โข โ
=
โ
|
13 | | seqomeq12 8312 |
. . . . . . 7
โข (((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) = (๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)) โง โ
= โ
) โ
seqฯ((๐
โ V, ๐ง โ V
โฆ (((๐ฅ
โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)) |
14 | 11, 12, 13 | sylancl 587 |
. . . . . 6
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
) = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)) |
15 | 14 | fveq1d 6802 |
. . . . 5
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ (seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) = (seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) |
16 | 15 | csbeq2dv 3844 |
. . . 4
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ) = โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) |
17 | 6, 16 | mpteq12dv 5172 |
. . 3
โข ((๐ฅ = ๐ด โง ๐ฆ = ๐ต) โ (๐ โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) = (๐ โ ๐ โฆ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |
18 | | df-cnf 9460 |
. . 3
โข CNF =
(๐ฅ โ On, ๐ฆ โ On โฆ (๐ โ {๐ โ (๐ฅ โm ๐ฆ) โฃ ๐ finSupp โ
} โฆ
โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ฅ โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |
19 | | ovex 7336 |
. . . . 5
โข (๐ด โm ๐ต) โ V |
20 | 5, 19 | rabex2 5267 |
. . . 4
โข ๐ โ V |
21 | 20 | mptex 7127 |
. . 3
โข (๐ โ ๐ โฆ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ)) โ V |
22 | 17, 18, 21 | ovmpoa 7456 |
. 2
โข ((๐ด โ On โง ๐ต โ On) โ (๐ด CNF ๐ต) = (๐ โ ๐ โฆ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |
23 | 1, 2, 22 | syl2anc 585 |
1
โข (๐ โ (๐ด CNF ๐ต) = (๐ โ ๐ โฆ โฆOrdIso( E , (๐ supp โ
)) / โโฆ(seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (โโ๐)) ยทo (๐โ(โโ๐))) +o ๐ง)), โ
)โdom โ))) |