This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Syntax definition wsmo

Description: Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.

		Ref	Expression
	Assertion	wsmo	wff Smo A