Theorem onsis

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

	Ref	Expression
Hypotheses	onsis.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	onsis.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
	onsis.3	⊢ ( 𝑥 ∈ Ons → ( ∀ 𝑦 ∈ Ons ( 𝑦 <s 𝑥 → 𝜓 ) → 𝜑 ) )
Assertion	onsis	⊢ ( 𝐴 ∈ Ons → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		onsis.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		onsis.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜒 ) )
3		onsis.3	⊢ ( 𝑥 ∈ Ons → ( ∀ 𝑦 ∈ Ons ( 𝑦 <s 𝑥 → 𝜓 ) → 𝜑 ) )
4		onswe	⊢ <s We Ons
5		onsse	⊢ <s Se Ons
6		vex	⊢ 𝑦 ∈ V
7	6	elpred	⊢ ( 𝑥 ∈ V → ( 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) ↔ ( 𝑦 ∈ Ons ∧ 𝑦 <s 𝑥 ) ) )
8	7	elv	⊢ ( 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) ↔ ( 𝑦 ∈ Ons ∧ 𝑦 <s 𝑥 ) )
9	8	imbi1i	⊢ ( ( 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) → 𝜓 ) ↔ ( ( 𝑦 ∈ Ons ∧ 𝑦 <s 𝑥 ) → 𝜓 ) )
10		impexp	⊢ ( ( ( 𝑦 ∈ Ons ∧ 𝑦 <s 𝑥 ) → 𝜓 ) ↔ ( 𝑦 ∈ Ons → ( 𝑦 <s 𝑥 → 𝜓 ) ) )
11	9 10	bitri	⊢ ( ( 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) → 𝜓 ) ↔ ( 𝑦 ∈ Ons → ( 𝑦 <s 𝑥 → 𝜓 ) ) )
12	11	ralbii2	⊢ ( ∀ 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) 𝜓 ↔ ∀ 𝑦 ∈ Ons ( 𝑦 <s 𝑥 → 𝜓 ) )
13	12 3	biimtrid	⊢ ( 𝑥 ∈ Ons → ( ∀ 𝑦 ∈ Pred ( <s , Ons , 𝑥 ) 𝜓 → 𝜑 ) )
14	4 5 1 2 13	wfis3	⊢ ( 𝐴 ∈ Ons → 𝜒 )