Metamath Proof Explorer

Theorem noinds

Description: Induction principle for a single surreal. If a property passes from a surreal's left and right sets to the surreal itself, then it holds for all surreals. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses noinds.1 ⊢ x = y → φ ↔ ψ
noinds.2 ⊢ x = A → φ ↔ χ
noinds.3 ⊢ x ∈ No → ∀ y ∈ L ⁡ x ∪ R ⁡ x ψ → φ
Assertion noinds ⊢ A ∈ No → χ

Proof

Step Hyp Ref Expression
1 noinds.1 ⊢ x = y → φ ↔ ψ
2 noinds.2 ⊢ x = A → φ ↔ χ
3 noinds.3 ⊢ x ∈ No → ∀ y ∈ L ⁡ x ∪ R ⁡ x ψ → φ
4 eqid ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b = a b | a ∈ L ⁡ b ∪ R ⁡ b
5 4 lrrecfr ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b Fr No
6 4 lrrecpo ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b Po No
7 4 lrrecse ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b Se No
8 5 6 7 3pm3.2i ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b Fr No ∧ a b | a ∈ L ⁡ b ∪ R ⁡ b Po No ∧ a b | a ∈ L ⁡ b ∪ R ⁡ b Se No
9 4 lrrecpred ⊢ x ∈ No → Pred a b | a ∈ L ⁡ b ∪ R ⁡ b No x = L ⁡ x ∪ R ⁡ x
10 9 raleqdv ⊢ x ∈ No → ∀ y ∈ Pred a b | a ∈ L ⁡ b ∪ R ⁡ b No x ψ ↔ ∀ y ∈ L ⁡ x ∪ R ⁡ x ψ
11 10 3 sylbid ⊢ x ∈ No → ∀ y ∈ Pred a b | a ∈ L ⁡ b ∪ R ⁡ b No x ψ → φ
12 11 1 2 frpoins3g ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b Fr No ∧ a b | a ∈ L ⁡ b ∪ R ⁡ b Po No ∧ a b | a ∈ L ⁡ b ∪ R ⁡ b Se No ∧ A ∈ No → χ
13 8 12 mpan ⊢ A ∈ No → χ