Theorem ons2ind

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

	Ref	Expression
Hypotheses	ons2ind.1	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝜑 ↔ 𝜓 ) )
	ons2ind.2	⊢ ( 𝑦 = 𝑦𝑂 → ( 𝜓 ↔ 𝜒 ) )
	ons2ind.3	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝜃 ↔ 𝜒 ) )
	ons2ind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
	ons2ind.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
	ons2ind.6	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → 𝜓 ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → 𝜃 ) ) → 𝜑 ) )
Assertion	ons2ind	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝜂 )

Proof

Step	Hyp	Ref	Expression
1		ons2ind.1	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝜑 ↔ 𝜓 ) )
2		ons2ind.2	⊢ ( 𝑦 = 𝑦𝑂 → ( 𝜓 ↔ 𝜒 ) )
3		ons2ind.3	⊢ ( 𝑥 = 𝑥𝑂 → ( 𝜃 ↔ 𝜒 ) )
4		ons2ind.4	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5		ons2ind.5	⊢ ( 𝑦 = 𝐵 → ( 𝜏 ↔ 𝜂 ) )
6		ons2ind.6	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → 𝜓 ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → 𝜃 ) ) → 𝜑 ) )
7		onswe	⊢ <s We Ons
8		wefr	⊢ ( <s We Ons → <s Fr Ons )
9	7 8	ax-mp	⊢ <s Fr Ons
10		weso	⊢ ( <s We Ons → <s Or Ons )
11		sopo	⊢ ( <s Or Ons → <s Po Ons )
12	7 10 11	mp2b	⊢ <s Po Ons
13		onsse	⊢ <s Se Ons
14		vex	⊢ 𝑥𝑂 ∈ V
15	14	elpred	⊢ ( 𝑥 ∈ V → ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ↔ ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) ) )
16	15	elv	⊢ ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ↔ ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) )
17		vex	⊢ 𝑦𝑂 ∈ V
18	17	elpred	⊢ ( 𝑦 ∈ V → ( 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ↔ ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) ) )
19	18	elv	⊢ ( 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ↔ ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) )
20	16 19	anbi12i	⊢ ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) ∧ ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) ) )
21		an4	⊢ ( ( ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) ∧ ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) ∧ ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) ) )
22	20 21	bitri	⊢ ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) ∧ ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) ) )
23	22	imbi1i	⊢ ( ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) → 𝜒 ) ↔ ( ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) ∧ ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) ) → 𝜒 ) )
24		impexp	⊢ ( ( ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) ∧ ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) ) → 𝜒 ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) → ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ) )
25	23 24	bitri	⊢ ( ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) → 𝜒 ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) → ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ) )
26	25	2albii	⊢ ( ∀ 𝑥𝑂 ∀ 𝑦𝑂 ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) → 𝜒 ) ↔ ∀ 𝑥𝑂 ∀ 𝑦𝑂 ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) → ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ) )
27		r2al	⊢ ( ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜒 ↔ ∀ 𝑥𝑂 ∀ 𝑦𝑂 ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∧ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) ) → 𝜒 ) )
28		r2al	⊢ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ↔ ∀ 𝑥𝑂 ∀ 𝑦𝑂 ( ( 𝑥𝑂 ∈ Ons ∧ 𝑦𝑂 ∈ Ons ) → ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ) )
29	26 27 28	3bitr4i	⊢ ( ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜒 ↔ ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) )
30	16	imbi1i	⊢ ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) → 𝜓 ) ↔ ( ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) → 𝜓 ) )
31		impexp	⊢ ( ( ( 𝑥𝑂 ∈ Ons ∧ 𝑥𝑂 <s 𝑥 ) → 𝜓 ) ↔ ( 𝑥𝑂 ∈ Ons → ( 𝑥𝑂 <s 𝑥 → 𝜓 ) ) )
32	30 31	bitri	⊢ ( ( 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) → 𝜓 ) ↔ ( 𝑥𝑂 ∈ Ons → ( 𝑥𝑂 <s 𝑥 → 𝜓 ) ) )
33	32	ralbii2	⊢ ( ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) 𝜓 ↔ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → 𝜓 ) )
34	19	imbi1i	⊢ ( ( 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) → 𝜃 ) ↔ ( ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) → 𝜃 ) )
35		impexp	⊢ ( ( ( 𝑦𝑂 ∈ Ons ∧ 𝑦𝑂 <s 𝑦 ) → 𝜃 ) ↔ ( 𝑦𝑂 ∈ Ons → ( 𝑦𝑂 <s 𝑦 → 𝜃 ) ) )
36	34 35	bitri	⊢ ( ( 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) → 𝜃 ) ↔ ( 𝑦𝑂 ∈ Ons → ( 𝑦𝑂 <s 𝑦 → 𝜃 ) ) )
37	36	ralbii2	⊢ ( ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜃 ↔ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → 𝜃 ) )
38	29 33 37	3anbi123i	⊢ ( ( ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜒 ∧ ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) 𝜓 ∧ ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜃 ) ↔ ( ∀ 𝑥𝑂 ∈ Ons ∀ 𝑦𝑂 ∈ Ons ( ( 𝑥𝑂 <s 𝑥 ∧ 𝑦𝑂 <s 𝑦 ) → 𝜒 ) ∧ ∀ 𝑥𝑂 ∈ Ons ( 𝑥𝑂 <s 𝑥 → 𝜓 ) ∧ ∀ 𝑦𝑂 ∈ Ons ( 𝑦𝑂 <s 𝑦 → 𝜃 ) ) )
39	38 6	biimtrid	⊢ ( ( 𝑥 ∈ Ons ∧ 𝑦 ∈ Ons ) → ( ( ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜒 ∧ ∀ 𝑥𝑂 ∈ Pred ( <s , Ons , 𝑥 ) 𝜓 ∧ ∀ 𝑦𝑂 ∈ Pred ( <s , Ons , 𝑦 ) 𝜃 ) → 𝜑 ) )
40	9 12 13 9 12 13 1 2 3 4 5 39	xpord2ind	⊢ ( ( 𝐴 ∈ Ons ∧ 𝐵 ∈ Ons ) → 𝜂 )