Step |
Hyp |
Ref |
Expression |
1 |
|
cantnffval.s |
โข ๐ = { ๐ โ ( ๐ด โm ๐ต ) โฃ ๐ finSupp โ
} |
2 |
|
cantnffval.a |
โข ( ๐ โ ๐ด โ On ) |
3 |
|
cantnffval.b |
โข ( ๐ โ ๐ต โ On ) |
4 |
1 2 3
|
cantnffval |
โข ( ๐ โ ( ๐ด CNF ๐ต ) = ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) ) |
5 |
4
|
dmeqd |
โข ( ๐ โ dom ( ๐ด CNF ๐ต ) = dom ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) ) |
6 |
|
fvex |
โข ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V |
7 |
6
|
csbex |
โข โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V |
8 |
7
|
rgenw |
โข โ ๐ โ ๐ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V |
9 |
|
dmmptg |
โข ( โ ๐ โ ๐ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) โ V โ dom ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) = ๐ ) |
10 |
8 9
|
ax-mp |
โข dom ( ๐ โ ๐ โฆ โฆ OrdIso ( E , ( ๐ supp โ
) ) / โ โฆ ( seqฯ ( ( ๐ โ V , ๐ง โ V โฆ ( ( ( ๐ด โo ( โ โ ๐ ) ) ยทo ( ๐ โ ( โ โ ๐ ) ) ) +o ๐ง ) ) , โ
) โ dom โ ) ) = ๐ |
11 |
5 10
|
eqtrdi |
โข ( ๐ โ dom ( ๐ด CNF ๐ต ) = ๐ ) |