Metamath Proof Explorer

Theorem no2inds

Description: Double induction on surreals. The many substitution instances are to cover all possible cases. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses no2inds.1 ⊢ x = z → φ ↔ ψ
no2inds.2 ⊢ y = w → ψ ↔ χ
no2inds.3 ⊢ x = z → θ ↔ χ
no2inds.4 ⊢ x = A → φ ↔ τ
no2inds.5 ⊢ y = B → τ ↔ η
no2inds.i ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ ∧ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ ∧ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ → φ
Assertion no2inds ⊢ A ∈ No ∧ B ∈ No → η

Proof

Step Hyp Ref Expression
1 no2inds.1 ⊢ x = z → φ ↔ ψ
2 no2inds.2 ⊢ y = w → ψ ↔ χ
3 no2inds.3 ⊢ x = z → θ ↔ χ
4 no2inds.4 ⊢ x = A → φ ↔ τ
5 no2inds.5 ⊢ y = B → τ ↔ η
6 no2inds.i ⊢ x ∈ No ∧ y ∈ No → ∀ z ∈ L ⁡ x ∪ R ⁡ x ∀ w ∈ L ⁡ y ∪ R ⁡ y χ ∧ ∀ z ∈ L ⁡ x ∪ R ⁡ x ψ ∧ ∀ w ∈ L ⁡ y ∪ R ⁡ y θ → φ
7 eqid ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b = a b | a ∈ L ⁡ b ∪ R ⁡ b
8 7 1 2 3 4 5 6 no2indlesm ⊢ A ∈ No ∧ B ∈ No → η