Metamath Proof Explorer

Theorem onsis

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

Ref Expression
Hypotheses onsis.1 ⊢ x = y → φ ↔ ψ
onsis.2 ⊢ x = A → φ ↔ χ
onsis.3 ⊢ x ∈ On s → ∀ y ∈ On s y < s x → ψ → φ
Assertion onsis ⊢ A ∈ On s → χ

Proof

Step Hyp Ref Expression
1 onsis.1 ⊢ x = y → φ ↔ ψ
2 onsis.2 ⊢ x = A → φ ↔ χ
3 onsis.3 ⊢ x ∈ On s → ∀ y ∈ On s y < s x → ψ → φ
4 onswe ⊢ < s We On s
5 onsse ⊢ < s Se On s
6 vex ⊢ y ∈ V
7 6 elpred ⊢ x ∈ V → y ∈ Pred < s On s x ↔ y ∈ On s ∧ y < s x
8 7 elv ⊢ y ∈ Pred < s On s x ↔ y ∈ On s ∧ y < s x
9 8 imbi1i ⊢ y ∈ Pred < s On s x → ψ ↔ y ∈ On s ∧ y < s x → ψ
10 impexp ⊢ y ∈ On s ∧ y < s x → ψ ↔ y ∈ On s → y < s x → ψ
11 9 10 bitri ⊢ y ∈ Pred < s On s x → ψ ↔ y ∈ On s → y < s x → ψ
12 11 ralbii2 ⊢ ∀ y ∈ Pred < s On s x ψ ↔ ∀ y ∈ On s y < s x → ψ
13 12 3 biimtrid ⊢ x ∈ On s → ∀ y ∈ Pred < s On s x ψ → φ
14 4 5 1 2 13 wfis3 ⊢ A ∈ On s → χ