Theorem ons2ind

Description: Double induction schema for surreal ordinals. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Hypotheses	ons2ind.1	No typesetting found for |- ( x = xO -> ( ph <-> ps ) ) with typecode |-
	ons2ind.2	No typesetting found for |- ( y = yO -> ( ps <-> ch ) ) with typecode |-
	ons2ind.3	No typesetting found for |- ( x = xO -> ( th <-> ch ) ) with typecode |-
	ons2ind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	ons2ind.5	$$⊢y=B\to \left(\tau \leftrightarrow \eta \right)$$
	ons2ind.6	No typesetting found for |- ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) /\ A. xO e. On_s ( xO ps ) /\ A. yO e. On_s ( yO th ) ) -> ph ) ) with typecode |-
Assertion	ons2ind	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \eta$$

Proof

Step	Hyp	Ref	Expression
1		ons2ind.1	Could not format ( x = xO -> ( ph <-> ps ) ) : No typesetting found for |- ( x = xO -> ( ph <-> ps ) ) with typecode |-
2		ons2ind.2	Could not format ( y = yO -> ( ps <-> ch ) ) : No typesetting found for |- ( y = yO -> ( ps <-> ch ) ) with typecode |-
3		ons2ind.3	Could not format ( x = xO -> ( th <-> ch ) ) : No typesetting found for |- ( x = xO -> ( th <-> ch ) ) with typecode |-
4		ons2ind.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		ons2ind.5	$$⊢y=B\to \left(\tau \leftrightarrow \eta \right)$$
6		ons2ind.6	Could not format ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) /\ A. xO e. On_s ( xO ps ) /\ A. yO e. On_s ( yO th ) ) -> ph ) ) : No typesetting found for |- ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) /\ A. xO e. On_s ( xO ps ) /\ A. yO e. On_s ( yO th ) ) -> ph ) ) with typecode |-
7		onswe	$$⊢{<}_s\mathrm{We}{On}_s$$
8		wefr	$$⊢{<}_s\mathrm{We}{On}_s\to {<}_s\mathrm{Fr}{On}_s$$
9	7 8	ax-mp	$$⊢{<}_s\mathrm{Fr}{On}_s$$
10		weso	$$⊢{<}_s\mathrm{We}{On}_s\to {<}_s\mathrm{Or}{On}_s$$
11		sopo	$$⊢{<}_s\mathrm{Or}{On}_s\to {<}_s\mathrm{Po}{On}_s$$
12	7 10 11	mp2b	$$⊢{<}_s\mathrm{Po}{On}_s$$
13		onsse	$$⊢{<}_s\mathrm{Se}{On}_s$$
14		vex	Could not format xO e. _V : No typesetting found for |- xO e. _V with typecode |-
15	14	elpred	Could not format ( x e. _V -> ( xO e. Pred ( ( xO e. On_s /\ xO ( xO e. Pred ( ( xO e. On_s /\ xO
16	15	elv	Could not format ( xO e. Pred ( ( xO e. On_s /\ xO ( xO e. On_s /\ xO
17		vex	Could not format yO e. _V : No typesetting found for |- yO e. _V with typecode |-
18	17	elpred	Could not format ( y e. _V -> ( yO e. Pred ( ( yO e. On_s /\ yO ( yO e. Pred ( ( yO e. On_s /\ yO
19	18	elv	Could not format ( yO e. Pred ( ( yO e. On_s /\ yO ( yO e. On_s /\ yO
20	16 19	anbi12i	Could not format ( ( xO e. Pred ( ( ( xO e. On_s /\ xO ( ( xO e. On_s /\ xO
21		an4	Could not format ( ( ( xO e. On_s /\ xO ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO
22	20 21	bitri	Could not format ( ( xO e. Pred ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO
23	22	imbi1i	Could not format ( ( ( xO e. Pred ( ch ) <-> ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) ) : No typesetting found for |- ( ( ( xO e. Pred ( ch ) <-> ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) ) with typecode |-
24		impexp	Could not format ( ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) : No typesetting found for |- ( ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) with typecode |-
25	23 24	bitri	Could not format ( ( ( xO e. Pred ( ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) : No typesetting found for |- ( ( ( xO e. Pred ( ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) with typecode |-
26	25	2albii	Could not format ( A. xO A. yO ( ( xO e. Pred ( ch ) <-> A. xO A. yO ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) : No typesetting found for |- ( A. xO A. yO ( ( xO e. Pred ( ch ) <-> A. xO A. yO ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) with typecode |-
27		r2al	Could not format ( A. xO e. Pred ( A. xO A. yO ( ( xO e. Pred ( ch ) ) : No typesetting found for |- ( A. xO e. Pred ( A. xO A. yO ( ( xO e. Pred ( ch ) ) with typecode |-
28		r2al	Could not format ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) <-> A. xO A. yO ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) : No typesetting found for |- ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) <-> A. xO A. yO ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) ) with typecode |-
29	26 27 28	3bitr4i	Could not format ( A. xO e. Pred ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) ) : No typesetting found for |- ( A. xO e. Pred ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) ) with typecode |-
30	16	imbi1i	Could not format ( ( xO e. Pred ( ps ) <-> ( ( xO e. On_s /\ xO ps ) ) : No typesetting found for |- ( ( xO e. Pred ( ps ) <-> ( ( xO e. On_s /\ xO ps ) ) with typecode |-
31		impexp	Could not format ( ( ( xO e. On_s /\ xO ps ) <-> ( xO e. On_s -> ( xO ps ) ) ) : No typesetting found for |- ( ( ( xO e. On_s /\ xO ps ) <-> ( xO e. On_s -> ( xO ps ) ) ) with typecode |-
32	30 31	bitri	Could not format ( ( xO e. Pred ( ps ) <-> ( xO e. On_s -> ( xO ps ) ) ) : No typesetting found for |- ( ( xO e. Pred ( ps ) <-> ( xO e. On_s -> ( xO ps ) ) ) with typecode |-
33	32	ralbii2	Could not format ( A. xO e. Pred ( A. xO e. On_s ( xO ps ) ) : No typesetting found for |- ( A. xO e. Pred ( A. xO e. On_s ( xO ps ) ) with typecode |-
34	19	imbi1i	Could not format ( ( yO e. Pred ( th ) <-> ( ( yO e. On_s /\ yO th ) ) : No typesetting found for |- ( ( yO e. Pred ( th ) <-> ( ( yO e. On_s /\ yO th ) ) with typecode |-
35		impexp	Could not format ( ( ( yO e. On_s /\ yO th ) <-> ( yO e. On_s -> ( yO th ) ) ) : No typesetting found for |- ( ( ( yO e. On_s /\ yO th ) <-> ( yO e. On_s -> ( yO th ) ) ) with typecode |-
36	34 35	bitri	Could not format ( ( yO e. Pred ( th ) <-> ( yO e. On_s -> ( yO th ) ) ) : No typesetting found for |- ( ( yO e. Pred ( th ) <-> ( yO e. On_s -> ( yO th ) ) ) with typecode |-
37	36	ralbii2	Could not format ( A. yO e. Pred ( A. yO e. On_s ( yO th ) ) : No typesetting found for |- ( A. yO e. Pred ( A. yO e. On_s ( yO th ) ) with typecode |-
38	29 33 37	3anbi123i	Could not format ( ( A. xO e. Pred ( ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) /\ A. xO e. On_s ( xO ps ) /\ A. yO e. On_s ( yO th ) ) ) : No typesetting found for |- ( ( A. xO e. Pred ( ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) /\ A. xO e. On_s ( xO ps ) /\ A. yO e. On_s ( yO th ) ) ) with typecode |-
39	38 6	biimtrid	Could not format ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. Pred ( ph ) ) : No typesetting found for |- ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. Pred ( ph ) ) with typecode |-
40	9 12 13 9 12 13 1 2 3 4 5 39	xpord2ind	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \eta$$