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 ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y = x y | x ∈ L ⁡ y ∪ R ⁡ y
13 12 lrrecfr ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Fr No
14 12 lrrecpo ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Po No
15 12 lrrecse ⊢ x y | x ∈ L ⁡ y ∪ R ⁡ y Se No
16 12 lrrecpred ⊢ a ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a = L ⁡ a ∪ R ⁡ a
17 16 3ad2ant1 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a = L ⁡ a ∪ R ⁡ a
18 12 lrrecpred ⊢ b ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b = L ⁡ b ∪ R ⁡ b
19 18 3ad2ant2 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b = L ⁡ b ∪ R ⁡ b
20 12 lrrecpred ⊢ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c = L ⁡ c ∪ R ⁡ c
21 20 3ad2ant3 ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c = L ⁡ c ∪ R ⁡ c
22 21 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c θ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c θ
23 19 22 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 θ
24 17 23 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 θ
25 19 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b χ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b χ
26 17 25 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 χ
27 21 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c ζ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c ζ
28 17 27 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 ζ
29 24 26 28 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 ζ
30 17 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ d ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No a ψ ↔ ∀ d ∈ L ⁡ a ∪ R ⁡ a ψ
31 21 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c τ ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c τ
32 19 31 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 τ
33 19 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ e ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No b σ ↔ ∀ e ∈ L ⁡ b ∪ R ⁡ b σ
34 30 32 33 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 σ
35 21 raleqdv ⊢ a ∈ No ∧ b ∈ No ∧ c ∈ No → ∀ f ∈ Pred x y | x ∈ L ⁡ y ∪ R ⁡ y No c η ↔ ∀ f ∈ L ⁡ c ∪ R ⁡ c η
36 29 34 35 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 η
37 36 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 η → φ
38 13 14 15 13 14 15 13 14 15 1 2 3 4 5 6 7 8 9 10 37 xpord3ind ⊢ X ∈ No ∧ Y ∈ No ∧ Z ∈ No → λ