Metamath Proof Explorer


Theorem cantnfdm

Description: The domain of the Cantor normal form function (in later lemmas we will use dom ( A CNF B ) to abbreviate "the set of finitely supported functions from B to A "). (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnffval.s โŠข ๐‘† = { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… }
cantnffval.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
cantnffval.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ On )
Assertion cantnfdm ( ๐œ‘ โ†’ dom ( ๐ด CNF ๐ต ) = ๐‘† )

Proof

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 ๐ต ) = ๐‘† )