Metamath Proof Explorer

Theorem cantnfsuc

Description: The value of the recursive function H at a successor. (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 cantnfsuc 
|- ( ( ph /\ K e. _om ) -> ( H ` suc K ) = ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) )

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 6 seqomsuc 
 |-  ( K e. _om -> ( H ` suc K ) = ( K ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) ( H ` K ) ) )
8 7 adantl 
 |-  ( ( ph /\ K e. _om ) -> ( H ` suc K ) = ( K ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) ( H ` K ) ) )
9 elex 
 |-  ( K e. _om -> K e. _V )
10 9 adantl 
 |-  ( ( ph /\ K e. _om ) -> K e. _V )
11 fvex 
 |-  ( H ` K ) e. _V
12 simpl 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> u = K )
13 12 fveq2d 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> ( G ` u ) = ( G ` K ) )
14 13 oveq2d 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> ( A ^o ( G ` u ) ) = ( A ^o ( G ` K ) ) )
15 13 fveq2d 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> ( F ` ( G ` u ) ) = ( F ` ( G ` K ) ) )
16 14 15 oveq12d 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) = ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) )
17 simpr 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> v = ( H ` K ) )
18 16 17 oveq12d 
 |-  ( ( u = K /\ v = ( H ` K ) ) -> ( ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o v ) = ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) )
19 fveq2 
 |-  ( k = u -> ( G ` k ) = ( G ` u ) )
20 19 oveq2d 
 |-  ( k = u -> ( A ^o ( G ` k ) ) = ( A ^o ( G ` u ) ) )
21 19 fveq2d 
 |-  ( k = u -> ( F ` ( G ` k ) ) = ( F ` ( G ` u ) ) )
22 20 21 oveq12d 
 |-  ( k = u -> ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) = ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) )
23 22 oveq1d 
 |-  ( k = u -> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) = ( ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o z ) )
24 oveq2 
 |-  ( z = v -> ( ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o z ) = ( ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o v ) )
25 23 24 cbvmpov 
 |-  ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) = ( u e. _V , v e. _V |-> ( ( ( A ^o ( G ` u ) ) .o ( F ` ( G ` u ) ) ) +o v ) )
26 ovex 
 |-  ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) e. _V
27 18 25 26 ovmpoa 
 |-  ( ( K e. _V /\ ( H ` K ) e. _V ) -> ( K ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) ( H ` K ) ) = ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) )
28 10 11 27 sylancl 
 |-  ( ( ph /\ K e. _om ) -> ( K ( k e. _V , z e. _V |-> ( ( ( A ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) +o z ) ) ( H ` K ) ) = ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) )
29 8 28 eqtrd 
 |-  ( ( ph /\ K e. _om ) -> ( H ` suc K ) = ( ( ( A ^o ( G ` K ) ) .o ( F ` ( G ` K ) ) ) +o ( H ` K ) ) )