| Step | Hyp | Ref | Expression | 
						
							| 1 |  | eqidd |  |-  ( x = A -> 1s = 1s ) | 
						
							| 2 |  | eqidd |  |-  ( x = A -> x.s = x.s ) | 
						
							| 3 |  | sneq |  |-  ( x = A -> { x } = { A } ) | 
						
							| 4 | 3 | xpeq2d |  |-  ( x = A -> ( NN_s X. { x } ) = ( NN_s X. { A } ) ) | 
						
							| 5 | 1 2 4 | seqseq123d |  |-  ( x = A -> seq_s 1s ( x.s , ( NN_s X. { x } ) ) = seq_s 1s ( x.s , ( NN_s X. { A } ) ) ) | 
						
							| 6 | 5 | fveq1d |  |-  ( x = A -> ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` y ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` y ) ) | 
						
							| 7 | 5 | fveq1d |  |-  ( x = A -> ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) ) | 
						
							| 8 | 7 | oveq2d |  |-  ( x = A -> ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { x } ) ) ` ( -us ` y ) ) ) = ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) ) ) | 
						
							| 9 | 6 8 | ifeq12d |  |-  ( x = A -> if ( 0s  | 
						
							| 10 | 9 | ifeq2d |  |-  ( x = A -> if ( y = 0s , 1s , if ( 0s  | 
						
							| 11 |  | eqeq1 |  |-  ( y = B -> ( y = 0s <-> B = 0s ) ) | 
						
							| 12 |  | breq2 |  |-  ( y = B -> ( 0s  0s  | 
						
							| 13 |  | fveq2 |  |-  ( y = B -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` y ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` B ) ) | 
						
							| 14 |  | 2fveq3 |  |-  ( y = B -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) ) | 
						
							| 15 | 14 | oveq2d |  |-  ( y = B -> ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` y ) ) ) = ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) ) ) | 
						
							| 16 | 12 13 15 | ifbieq12d |  |-  ( y = B -> if ( 0s  | 
						
							| 17 | 11 16 | ifbieq2d |  |-  ( y = B -> if ( y = 0s , 1s , if ( 0s  | 
						
							| 18 |  | df-exps |  |-  ^su = ( x e. No , y e. ZZ_s |-> if ( y = 0s , 1s , if ( 0s  | 
						
							| 19 |  | 1sno |  |-  1s e. No | 
						
							| 20 | 19 | elexi |  |-  1s e. _V | 
						
							| 21 |  | fvex |  |-  ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` B ) e. _V | 
						
							| 22 |  | ovex |  |-  ( 1s /su ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` ( -us ` B ) ) ) e. _V | 
						
							| 23 | 21 22 | ifex |  |-  if ( 0s  | 
						
							| 24 | 20 23 | ifex |  |-  if ( B = 0s , 1s , if ( 0s  | 
						
							| 25 | 10 17 18 24 | ovmpo |  |-  ( ( A e. No /\ B e. ZZ_s ) -> ( A ^su B ) = if ( B = 0s , 1s , if ( 0s  |