Metamath Proof Explorer


Theorem cantnff

Description: The CNF function is a function from finitely supported functions from B to A , to the ordinal exponential A ^o B . (Contributed by Mario Carneiro, 28-May-2015)

Ref Expression
Hypotheses cantnfs.s โŠข ๐‘† = dom ( ๐ด CNF ๐ต )
cantnfs.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
cantnfs.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ On )
Assertion cantnff ( ๐œ‘ โ†’ ( ๐ด CNF ๐ต ) : ๐‘† โŸถ ( ๐ด โ†‘o ๐ต ) )

Proof

Step Hyp Ref Expression
1 cantnfs.s โŠข ๐‘† = dom ( ๐ด CNF ๐ต )
2 cantnfs.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ On )
3 cantnfs.b โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ On )
4 fvex โŠข ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) โˆˆ V
5 4 csbex โŠข โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) โˆˆ V
6 5 a1i โŠข ( ( ๐œ‘ โˆง ๐‘“ โˆˆ ๐‘† ) โ†’ โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) โˆˆ V )
7 eqid โŠข { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… } = { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… }
8 7 2 3 cantnffval โŠข ( ๐œ‘ โ†’ ( ๐ด CNF ๐ต ) = ( ๐‘“ โˆˆ { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… } โ†ฆ โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) ) )
9 7 2 3 cantnfdm โŠข ( ๐œ‘ โ†’ dom ( ๐ด CNF ๐ต ) = { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… } )
10 1 9 eqtrid โŠข ( ๐œ‘ โ†’ ๐‘† = { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… } )
11 10 mpteq1d โŠข ( ๐œ‘ โ†’ ( ๐‘“ โˆˆ ๐‘† โ†ฆ โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) ) = ( ๐‘“ โˆˆ { ๐‘” โˆˆ ( ๐ด โ†‘m ๐ต ) โˆฃ ๐‘” finSupp โˆ… } โ†ฆ โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) ) )
12 8 11 eqtr4d โŠข ( ๐œ‘ โ†’ ( ๐ด CNF ๐ต ) = ( ๐‘“ โˆˆ ๐‘† โ†ฆ โฆ‹ OrdIso ( E , ( ๐‘“ supp โˆ… ) ) / โ„Ž โฆŒ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( โ„Ž โ€˜ ๐‘˜ ) ) ยทo ( ๐‘“ โ€˜ ( โ„Ž โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom โ„Ž ) ) )
13 2 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ๐ด โˆˆ On )
14 3 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ๐ต โˆˆ On )
15 eqid โŠข OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) = OrdIso ( E , ( ๐‘ฅ supp โˆ… ) )
16 simpr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ๐‘ฅ โˆˆ ๐‘† )
17 eqid โŠข seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) = seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… )
18 1 13 14 15 16 17 cantnfval โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) = ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) ) )
19 18 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) = ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) ) )
20 ovex โŠข ( ๐‘ฅ supp โˆ… ) โˆˆ V
21 1 13 14 15 16 cantnfcl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( E We ( ๐‘ฅ supp โˆ… ) โˆง dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โˆˆ ฯ‰ ) )
22 21 simpld โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ E We ( ๐‘ฅ supp โˆ… ) )
23 15 oien โŠข ( ( ( ๐‘ฅ supp โˆ… ) โˆˆ V โˆง E We ( ๐‘ฅ supp โˆ… ) ) โ†’ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ‰ˆ ( ๐‘ฅ supp โˆ… ) )
24 20 22 23 sylancr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ‰ˆ ( ๐‘ฅ supp โˆ… ) )
25 24 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ‰ˆ ( ๐‘ฅ supp โˆ… ) )
26 suppssdm โŠข ( ๐‘ฅ supp โˆ… ) โŠ† dom ๐‘ฅ
27 1 2 3 cantnfs โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘† โ†” ( ๐‘ฅ : ๐ต โŸถ ๐ด โˆง ๐‘ฅ finSupp โˆ… ) ) )
28 27 simprbda โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ๐‘ฅ : ๐ต โŸถ ๐ด )
29 26 28 fssdm โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( ๐‘ฅ supp โˆ… ) โŠ† ๐ต )
30 feq3 โŠข ( ๐ด = โˆ… โ†’ ( ๐‘ฅ : ๐ต โŸถ ๐ด โ†” ๐‘ฅ : ๐ต โŸถ โˆ… ) )
31 28 30 syl5ibcom โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( ๐ด = โˆ… โ†’ ๐‘ฅ : ๐ต โŸถ โˆ… ) )
32 31 imp โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ๐‘ฅ : ๐ต โŸถ โˆ… )
33 f00 โŠข ( ๐‘ฅ : ๐ต โŸถ โˆ… โ†” ( ๐‘ฅ = โˆ… โˆง ๐ต = โˆ… ) )
34 32 33 sylib โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ๐‘ฅ = โˆ… โˆง ๐ต = โˆ… ) )
35 34 simprd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ๐ต = โˆ… )
36 sseq0 โŠข ( ( ( ๐‘ฅ supp โˆ… ) โŠ† ๐ต โˆง ๐ต = โˆ… ) โ†’ ( ๐‘ฅ supp โˆ… ) = โˆ… )
37 29 35 36 syl2an2r โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ๐‘ฅ supp โˆ… ) = โˆ… )
38 25 37 breqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ‰ˆ โˆ… )
39 en0 โŠข ( dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ‰ˆ โˆ… โ†” dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) = โˆ… )
40 38 39 sylib โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) = โˆ… )
41 40 fveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ dom OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) ) = ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ โˆ… ) )
42 0ex โŠข โˆ… โˆˆ V
43 17 seqom0g โŠข ( โˆ… โˆˆ V โ†’ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ โˆ… ) = โˆ… )
44 42 43 mp1i โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( seqฯ‰ ( ( ๐‘˜ โˆˆ V , ๐‘ง โˆˆ V โ†ฆ ( ( ( ๐ด โ†‘o ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ยทo ( ๐‘ฅ โ€˜ ( OrdIso ( E , ( ๐‘ฅ supp โˆ… ) ) โ€˜ ๐‘˜ ) ) ) +o ๐‘ง ) ) , โˆ… ) โ€˜ โˆ… ) = โˆ… )
45 19 41 44 3eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) = โˆ… )
46 el1o โŠข ( ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) โˆˆ 1o โ†” ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) = โˆ… )
47 45 46 sylibr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) โˆˆ 1o )
48 35 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ๐ด โ†‘o ๐ต ) = ( ๐ด โ†‘o โˆ… ) )
49 13 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ๐ด โˆˆ On )
50 oe0 โŠข ( ๐ด โˆˆ On โ†’ ( ๐ด โ†‘o โˆ… ) = 1o )
51 49 50 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ๐ด โ†‘o โˆ… ) = 1o )
52 48 51 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ๐ด โ†‘o ๐ต ) = 1o )
53 47 52 eleqtrrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด = โˆ… ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐ด โ†‘o ๐ต ) )
54 13 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ ๐ด โˆˆ On )
55 14 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ ๐ต โˆˆ On )
56 16 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ ๐‘ฅ โˆˆ ๐‘† )
57 on0eln0 โŠข ( ๐ด โˆˆ On โ†’ ( โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ… ) )
58 13 57 syl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( โˆ… โˆˆ ๐ด โ†” ๐ด โ‰  โˆ… ) )
59 58 biimpar โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ โˆ… โˆˆ ๐ด )
60 29 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ ( ๐‘ฅ supp โˆ… ) โŠ† ๐ต )
61 1 54 55 56 59 55 60 cantnflt2 โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โˆง ๐ด โ‰  โˆ… ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐ด โ†‘o ๐ต ) )
62 53 61 pm2.61dane โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† ) โ†’ ( ( ๐ด CNF ๐ต ) โ€˜ ๐‘ฅ ) โˆˆ ( ๐ด โ†‘o ๐ต ) )
63 6 12 62 fmpt2d โŠข ( ๐œ‘ โ†’ ( ๐ด CNF ๐ต ) : ๐‘† โŸถ ( ๐ด โ†‘o ๐ต ) )