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 
|- ( ph -> A e. On )
cantnfs.b 
|- ( ph -> B e. On )
cantnfcl.g 
|- G = OrdIso ( _E , ( F supp (/) ) )
cantnfcl.f 
|- ( ph -> F e. S )
cantnfval.h 
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) )
Assertion cantnfval2 
|- ( ph -> ( ( A CNF B ) ` F ) = ( seqom ( ( k e. dom G , z e. On |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) , (/) ) ` dom G ) )

Proof

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