Metamath Proof Explorer

Theorem no3inds

Description: Triple induction over surreal numbers. (Contributed by Scott Fenton, 9-Oct-2024)

Ref Expression
Hypotheses no3inds.1 ⊢ a = d → φ ↔ ψ
no3inds.2 ⊢ b = e → ψ ↔ χ
no3inds.3 ⊢ c = f → χ ↔ θ
no3inds.4 ⊢ a = d → τ ↔ θ
no3inds.5 ⊢ b = e → η ↔ τ
no3inds.6 ⊢ b = e → ζ ↔ θ
no3inds.7 ⊢ c = f → σ ↔ τ
no3inds.8 ⊢ a = X → φ ↔ ρ
no3inds.9 ⊢ b = Y → ρ ↔ μ
no3inds.10 ⊢ c = Z → μ ↔ λ
no3inds.i ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b χ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c τ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ ∧ ∀ f ∈ L ⁡ c ∪ R ⁡ c η → φ
Assertion no3inds ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → λ

Proof

Step Hyp Ref Expression
1 no3inds.1 ⊢ a = d → φ ↔ ψ
2 no3inds.2 ⊢ b = e → ψ ↔ χ
3 no3inds.3 ⊢ c = f → χ ↔ θ
4 no3inds.4 ⊢ a = d → τ ↔ θ
5 no3inds.5 ⊢ b = e → η ↔ τ
6 no3inds.6 ⊢ b = e → ζ ↔ θ
7 no3inds.7 ⊢ c = f → σ ↔ τ
8 no3inds.8 ⊢ a = X → φ ↔ ρ
9 no3inds.9 ⊢ b = Y → ρ ↔ μ
10 no3inds.10 ⊢ c = Z → μ ↔ λ
11 no3inds.i ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b χ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c τ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ ∧ ∀ f ∈ L ⁡ c ∪ R ⁡ c η → φ
12 eqid ⊢ z w | z ∈ No × No × No ∧ w ∈ No × No × No ∧ 1 st ⁡ 1 st ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 1 st ⁡ 1 st ⁡ w ∨ 1 st ⁡ 1 st ⁡ z = 1 st ⁡ 1 st ⁡ w ∧ 2 nd ⁡ 1 st ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 2 nd ⁡ 1 st ⁡ w ∨ 2 nd ⁡ 1 st ⁡ z = 2 nd ⁡ 1 st ⁡ w ∧ 2 nd ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 2 nd ⁡ w ∨ 2 nd ⁡ z = 2 nd ⁡ w ∧ z ≠ w = z w | z ∈ No × No × No ∧ w ∈ No × No × No ∧ 1 st ⁡ 1 st ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 1 st ⁡ 1 st ⁡ w ∨ 1 st ⁡ 1 st ⁡ z = 1 st ⁡ 1 st ⁡ w ∧ 2 nd ⁡ 1 st ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 2 nd ⁡ 1 st ⁡ w ∨ 2 nd ⁡ 1 st ⁡ z = 2 nd ⁡ 1 st ⁡ w ∧ 2 nd ⁡ z x y | x ∈ L ⁡ y ∪ R ⁡ y 2 nd ⁡ w ∨ 2 nd ⁡ z = 2 nd ⁡ w ∧ z ≠ w
13 eqid ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y = x y | x ∈ L ⁡ y ∪ R ⁡ y
14 13 lrrecfr ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Fr No
15 13 lrrecpo ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Po No
16 13 lrrecse ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Se No
17 13 lrrecpred ⊢ a ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a = L ⁡ a ∪ R ⁡ a
18 17 3ad2ant1 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a = L ⁡ a ∪ R ⁡ a
19 13 lrrecpred ⊢ b ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b = L ⁡ b ∪ R ⁡ b
20 19 3ad2ant2 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b = L ⁡ b ∪ R ⁡ b
21 13 lrrecpred ⊢ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c = L ⁡ c ∪ R ⁡ c
22 21 3ad2ant3 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c = L ⁡ c ∪ R ⁡ c
23 22 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c θ
24 20 23 raleqbidv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ
25 18 24 raleqbidv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ
26 20 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b χ
27 18 26 raleqbidv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b χ
28 22 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ
29 18 28 raleqbidv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ
30 25 27 29 3anbi123d ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b χ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ
31 18 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ψ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ
32 22 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c τ
33 20 32 raleqbidv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c τ
34 20 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b σ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ
35 31 33 34 3anbi123d ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ψ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b σ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c τ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ
36 22 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c η ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c η
37 30 35 36 3anbi123d ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ψ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b σ ∧ ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c η ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c θ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ e ∈ L ⁡ b ∪ R ⁡ b χ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ ∧ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b ∀ f ∈ L ⁡ c ∪ R ⁡ c τ ∧ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ ∧ ∀ f ∈ L ⁡ c ∪ R ⁡ c η
38 37 11 sylbid ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ∧ ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ψ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ∧ ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b σ ∧ ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c η → φ
39 12 14 15 16 14 15 16 14 15 16 1 2 3 4 5 6 7 8 9 10 38 xpord3ind ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → λ