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 eqid ⊢ c d | c ∈ No × No ∧ d ∈ No × No ∧ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 1 st ⁡ d ∨ 1 st ⁡ c = 1 st ⁡ d ∧ 2 nd ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 2 nd ⁡ d ∨ 2 nd ⁡ c = 2 nd ⁡ d ∧ c ≠ d = c d | c ∈ No × No ∧ d ∈ No × No ∧ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 1 st ⁡ d ∨ 1 st ⁡ c = 1 st ⁡ d ∧ 2 nd ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 2 nd ⁡ d ∨ 2 nd ⁡ c = 2 nd ⁡ d ∧ c ≠ d
9 7 8 1 2 3 4 5 6 no2indslem ⊢ A ∈ No ∧ B ∈ No → η