Theorem onsis

Description: Transfinite induction schema for surreal ordinals. (Contributed by Scott Fenton, 6-Nov-2025)

	Ref	Expression
Hypotheses	onsis.1	|- ( x = y -> ( ph <-> ps ) )
	onsis.2	|- ( x = A -> ( ph <-> ch ) )
	onsis.3	|- ( x e. On_s -> ( A. y e. On_s ( y ps ) -> ph ) )
Assertion	onsis	|- ( A e. On_s -> ch )

Proof

Step	Hyp	Ref	Expression
1		onsis.1	|- ( x = y -> ( ph <-> ps ) )
2		onsis.2	|- ( x = A -> ( ph <-> ch ) )
3		onsis.3	|- ( x e. On_s -> ( A. y e. On_s ( y ps ) -> ph ) )
4		onswe	|-
5		onsse	|-
6		vex	|- y e. _V
7	6	elpred	|- ( x e. _V -> ( y e. Pred ( ( y e. On_s /\ y
8	7	elv	|- ( y e. Pred ( ( y e. On_s /\ y
9	8	imbi1i	|- ( ( y e. Pred ( ps ) <-> ( ( y e. On_s /\ y ps ) )
10		impexp	|- ( ( ( y e. On_s /\ y ps ) <-> ( y e. On_s -> ( y ps ) ) )
11	9 10	bitri	|- ( ( y e. Pred ( ps ) <-> ( y e. On_s -> ( y ps ) ) )
12	11	ralbii2	|- ( A. y e. Pred ( A. y e. On_s ( y ps ) )
13	12 3	biimtrid	|- ( x e. On_s -> ( A. y e. Pred ( ph ) )
14	4 5 1 2 13	wfis3	|- ( A e. On_s -> ch )