Metamath Proof Explorer


Theorem cantnfval2

Description: Alternate expression for the value of the Cantor normal form function. (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s S = dom A CNF B
cantnfs.a φ A On
cantnfs.b φ B On
cantnfcl.g G = OrdIso E F supp
cantnfcl.f φ F S
cantnfval.h H = seq ω k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z
Assertion cantnfval2 φ A CNF B F = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G

Proof

Step Hyp Ref Expression
1 cantnfs.s S = dom A CNF B
2 cantnfs.a φ A On
3 cantnfs.b φ B On
4 cantnfcl.g G = OrdIso E F supp
5 cantnfcl.f φ F S
6 cantnfval.h H = seq ω k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z
7 1 2 3 4 5 6 cantnfval φ A CNF B F = H dom G
8 ssid dom G dom G
9 1 2 3 4 5 cantnfcl φ E We supp F dom G ω
10 9 simprd φ dom G ω
11 sseq1 u = u dom G dom G
12 fveq2 u = H u = H
13 0ex V
14 6 seqom0g V H =
15 13 14 ax-mp H =
16 12 15 eqtrdi u = H u =
17 fveq2 u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z
18 eqid seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z
19 18 seqom0g V seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z =
20 13 19 ax-mp seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z =
21 17 20 eqtrdi u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u =
22 16 21 eqeq12d u = H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u =
23 11 22 imbi12d u = u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u dom G =
24 23 imbi2d u = φ u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u φ dom G =
25 sseq1 u = v u dom G v dom G
26 fveq2 u = v H u = H v
27 fveq2 u = v seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
28 26 27 eqeq12d u = v H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
29 25 28 imbi12d u = v u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
30 29 imbi2d u = v φ u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u φ v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
31 sseq1 u = suc v u dom G suc v dom G
32 fveq2 u = suc v H u = H suc v
33 fveq2 u = suc v seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
34 32 33 eqeq12d u = suc v H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
35 31 34 imbi12d u = suc v u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
36 35 imbi2d u = suc v φ u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u φ suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
37 sseq1 u = dom G u dom G dom G dom G
38 fveq2 u = dom G H u = H dom G
39 fveq2 u = dom G seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
40 38 39 eqeq12d u = dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
41 37 40 imbi12d u = dom G u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u dom G dom G H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
42 41 imbi2d u = dom G φ u dom G H u = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z u φ dom G dom G H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
43 eqid =
44 43 2a1i φ dom G =
45 sssucid v suc v
46 sstr v suc v suc v dom G v dom G
47 45 46 mpan suc v dom G v dom G
48 47 imim1i v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v suc v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
49 oveq2 H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z H v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
50 6 seqomsuc v ω H suc v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z H v
51 50 ad2antrl φ v ω suc v dom G H suc v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z H v
52 18 seqomsuc v ω seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v = v k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
53 52 ad2antrl φ v ω suc v dom G seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v = v k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
54 ssv dom G V
55 ssv On V
56 resmpo dom G V On V k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z dom G × On = k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z
57 54 55 56 mp2an k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z dom G × On = k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z
58 57 oveqi v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z dom G × On seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v = v k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
59 simprr φ v ω suc v dom G suc v dom G
60 vex v V
61 60 sucid v suc v
62 61 a1i φ v ω suc v dom G v suc v
63 59 62 sseldd φ v ω suc v dom G v dom G
64 18 cantnfvalf seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z : ω On
65 64 ffvelrni v ω seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v On
66 65 ad2antrl φ v ω suc v dom G seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v On
67 ovres v dom G seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v On v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z dom G × On seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
68 63 66 67 syl2anc φ v ω suc v dom G v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z dom G × On seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
69 58 68 eqtr3id φ v ω suc v dom G v k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
70 53 69 eqtrd φ v ω suc v dom G seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
71 51 70 eqeq12d φ v ω suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z H v = v k V , z V A 𝑜 G k 𝑜 F G k + 𝑜 z seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v
72 49 71 syl5ibr φ v ω suc v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
73 72 expr φ v ω suc v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
74 73 a2d φ v ω suc v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
75 48 74 syl5 φ v ω v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
76 75 expcom v ω φ v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
77 76 a2d v ω φ v dom G H v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z v φ suc v dom G H suc v = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z suc v
78 24 30 36 42 44 77 finds dom G ω φ dom G dom G H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
79 10 78 mpcom φ dom G dom G H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
80 8 79 mpi φ H dom G = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G
81 7 80 eqtrd φ A CNF B F = seq ω k dom G , z On A 𝑜 G k 𝑜 F G k + 𝑜 z dom G