Theorem ons2ind

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

	Ref	Expression
Hypotheses	ons2ind.1	|- ( x = xO -> ( ph <-> ps ) )
	ons2ind.2	|- ( y = yO -> ( ps <-> ch ) )
	ons2ind.3	|- ( x = xO -> ( th <-> ch ) )
	ons2ind.4	|- ( x = A -> ( ph <-> ta ) )
	ons2ind.5	|- ( y = B -> ( ta <-> et ) )
	ons2ind.6	|- ( ( 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 ) )
Assertion	ons2ind	|- ( ( A e. On_s /\ B e. On_s ) -> et )

Proof

Step	Hyp	Ref	Expression
1		ons2ind.1	|- ( x = xO -> ( ph <-> ps ) )
2		ons2ind.2	|- ( y = yO -> ( ps <-> ch ) )
3		ons2ind.3	|- ( x = xO -> ( th <-> ch ) )
4		ons2ind.4	|- ( x = A -> ( ph <-> ta ) )
5		ons2ind.5	|- ( y = B -> ( ta <-> et ) )
6		ons2ind.6	|- ( ( 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 ) )
7		onswe	|-
8		wefr	|- (
9	7 8	ax-mp	|-
10		weso	|- (
11		sopo	|- (
12	7 10 11	mp2b	|-
13		onsse	|-
14		vex	|- xO e. _V
15	14	elpred	|- ( x e. _V -> ( xO e. Pred ( ( xO e. On_s /\ xO
16	15	elv	|- ( xO e. Pred ( ( xO e. On_s /\ xO
17		vex	|- yO e. _V
18	17	elpred	|- ( y e. _V -> ( yO e. Pred ( ( yO e. On_s /\ yO
19	18	elv	|- ( yO e. Pred ( ( yO e. On_s /\ yO
20	16 19	anbi12i	|- ( ( xO e. Pred ( ( ( xO e. On_s /\ xO
21		an4	|- ( ( ( xO e. On_s /\ xO ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO
22	20 21	bitri	|- ( ( xO e. Pred ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO
23	22	imbi1i	|- ( ( ( xO e. Pred ( ch ) <-> ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) )
24		impexp	|- ( ( ( ( xO e. On_s /\ yO e. On_s ) /\ ( xO ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) )
25	23 24	bitri	|- ( ( ( xO e. Pred ( ch ) <-> ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) )
26	25	2albii	|- ( A. xO A. yO ( ( xO e. Pred ( ch ) <-> A. xO A. yO ( ( xO e. On_s /\ yO e. On_s ) -> ( ( xO ch ) ) )
27		r2al	|- ( A. xO e. Pred ( A. xO A. yO ( ( xO e. Pred ( ch ) )
28		r2al	|- ( 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 ) ) )
29	26 27 28	3bitr4i	|- ( A. xO e. Pred ( A. xO e. On_s A. yO e. On_s ( ( xO ch ) )
30	16	imbi1i	|- ( ( xO e. Pred ( ps ) <-> ( ( xO e. On_s /\ xO ps ) )
31		impexp	|- ( ( ( xO e. On_s /\ xO ps ) <-> ( xO e. On_s -> ( xO ps ) ) )
32	30 31	bitri	|- ( ( xO e. Pred ( ps ) <-> ( xO e. On_s -> ( xO ps ) ) )
33	32	ralbii2	|- ( A. xO e. Pred ( A. xO e. On_s ( xO ps ) )
34	19	imbi1i	|- ( ( yO e. Pred ( th ) <-> ( ( yO e. On_s /\ yO th ) )
35		impexp	|- ( ( ( yO e. On_s /\ yO th ) <-> ( yO e. On_s -> ( yO th ) ) )
36	34 35	bitri	|- ( ( yO e. Pred ( th ) <-> ( yO e. On_s -> ( yO th ) ) )
37	36	ralbii2	|- ( A. yO e. Pred ( A. yO e. On_s ( yO th ) )
38	29 33 37	3anbi123i	|- ( ( 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 ) ) )
39	38 6	biimtrid	|- ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. Pred ( ph ) )
40	9 12 13 9 12 13 1 2 3 4 5 39	xpord2ind	|- ( ( A e. On_s /\ B e. On_s ) -> et )