Metamath Proof Explorer

Theorem no3inds

Description: Triple induction over surreal numbers. The substitution instances cover all possible instances of less than or equal to x, y, and z. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses no3inds.1 ⊢ p = q → φ ↔ ψ
no3inds.2 ⊢ p = x y z → φ ↔ χ
no3inds.3 ⊢ q = w t u → ψ ↔ θ
no3inds.4 ⊢ u = z → θ ↔ τ
no3inds.5 ⊢ t = y → θ ↔ η
no3inds.6 ⊢ u = z → η ↔ ζ
no3inds.7 ⊢ w = x → θ ↔ σ
no3inds.8 ⊢ u = z → σ ↔ ρ
no3inds.9 ⊢ t = y → σ ↔ μ
no3inds.10 ⊢ x = A → χ ↔ λ
no3inds.11 ⊢ y = B → λ ↔ κ
no3inds.12 No typesetting found for |- ( z = C -> ( ka <-> al ) ) with typecode |-
no3inds.i ⊢ x ∈ No ∧ y ∈ No ∧ z ∈ No → ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ t ∈ L ⁡ y ∪ R ⁡ y ∀ u ∈ L ⁡ z ∪ R ⁡ z θ ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ t ∈ L ⁡ y ∪ R ⁡ y τ ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ u ∈ L ⁡ z ∪ R ⁡ z η ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ζ ∧ ∀ t ∈ L ⁡ y ∪ R ⁡ y ∀ u ∈ L ⁡ z ∪ R ⁡ z σ ∧ ∀ t ∈ L ⁡ y ∪ R ⁡ y ρ ∧ ∀ u ∈ L ⁡ z ∪ R ⁡ z μ → χ
Assertion no3inds Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> al ) with typecode |-

Proof

Step Hyp Ref Expression
1 no3inds.1 ⊢ p = q → φ ↔ ψ
2 no3inds.2 ⊢ p = x y z → φ ↔ χ
3 no3inds.3 ⊢ q = w t u → ψ ↔ θ
4 no3inds.4 ⊢ u = z → θ ↔ τ
5 no3inds.5 ⊢ t = y → θ ↔ η
6 no3inds.6 ⊢ u = z → η ↔ ζ
7 no3inds.7 ⊢ w = x → θ ↔ σ
8 no3inds.8 ⊢ u = z → σ ↔ ρ
9 no3inds.9 ⊢ t = y → σ ↔ μ
10 no3inds.10 ⊢ x = A → χ ↔ λ
11 no3inds.11 ⊢ y = B → λ ↔ κ
12 no3inds.12 Could not format ( z = C -> ( ka <-> al ) ) : No typesetting found for |- ( z = C -> ( ka <-> al ) ) with typecode |-
13 no3inds.i ⊢ x ∈ No ∧ y ∈ No ∧ z ∈ No → ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ t ∈ L ⁡ y ∪ R ⁡ y ∀ u ∈ L ⁡ z ∪ R ⁡ z θ ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ t ∈ L ⁡ y ∪ R ⁡ y τ ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ∀ u ∈ L ⁡ z ∪ R ⁡ z η ∧ ∀ w ∈ L ⁡ x ∪ R ⁡ x ζ ∧ ∀ t ∈ L ⁡ y ∪ R ⁡ y ∀ u ∈ L ⁡ z ∪ R ⁡ z σ ∧ ∀ t ∈ L ⁡ y ∪ R ⁡ y ρ ∧ ∀ u ∈ L ⁡ z ∪ R ⁡ z μ → χ
14 eqid ⊢ a b | a ∈ L ⁡ b ∪ R ⁡ b = a b | a ∈ L ⁡ b ∪ R ⁡ b
15 eqid ⊢ c d | c ∈ No × No × No ∧ d ∈ No × No × No ∧ 1 st ⁡ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 1 st ⁡ 1 st ⁡ d ∨ 1 st ⁡ 1 st ⁡ c = 1 st ⁡ 1 st ⁡ d ∧ 2 nd ⁡ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 2 nd ⁡ 1 st ⁡ d ∨ 2 nd ⁡ 1 st ⁡ c = 2 nd ⁡ 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 × No ∧ d ∈ No × No × No ∧ 1 st ⁡ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 1 st ⁡ 1 st ⁡ d ∨ 1 st ⁡ 1 st ⁡ c = 1 st ⁡ 1 st ⁡ d ∧ 2 nd ⁡ 1 st ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 2 nd ⁡ 1 st ⁡ d ∨ 2 nd ⁡ 1 st ⁡ c = 2 nd ⁡ 1 st ⁡ d ∧ 2 nd ⁡ c a b | a ∈ L ⁡ b ∪ R ⁡ b 2 nd ⁡ d ∨ 2 nd ⁡ c = 2 nd ⁡ d ∧ c ≠ d
16 14 15 1 2 3 4 5 6 7 8 9 10 11 12 13 no3indslem Could not format ( ( A e. No /\ B e. No /\ C e. No ) -> al ) : No typesetting found for |- ( ( A e. No /\ B e. No /\ C e. No ) -> al ) with typecode |-