| Step | Hyp | Ref | Expression | 
						
							| 1 |  | df-n0s |  |-  NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) | 
						
							| 2 | 1 | a1i |  |-  ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s = ( rec ( ( n e. _V |-> ( n +s 1s ) ) , 0s ) " _om ) ) | 
						
							| 3 |  | 0sno |  |-  0s e. No | 
						
							| 4 | 3 | a1i |  |-  ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> 0s e. No ) | 
						
							| 5 |  | simpl |  |-  ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> 0s e. A ) | 
						
							| 6 |  | oveq1 |  |-  ( x = y -> ( x +s 1s ) = ( y +s 1s ) ) | 
						
							| 7 | 6 | eleq1d |  |-  ( x = y -> ( ( x +s 1s ) e. A <-> ( y +s 1s ) e. A ) ) | 
						
							| 8 | 7 | rspccva |  |-  ( ( A. x e. A ( x +s 1s ) e. A /\ y e. A ) -> ( y +s 1s ) e. A ) | 
						
							| 9 | 8 | adantll |  |-  ( ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) /\ y e. A ) -> ( y +s 1s ) e. A ) | 
						
							| 10 | 2 4 5 9 | noseqind |  |-  ( ( 0s e. A /\ A. x e. A ( x +s 1s ) e. A ) -> NN0_s C_ A ) |