Metamath Proof Explorer

Theorem on3ind

Description: Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 on3ind.1 ⊢ a = d → φ ↔ ψ
2 on3ind.2 ⊢ b = e → ψ ↔ χ
3 on3ind.3 ⊢ c = f → χ ↔ θ
4 on3ind.4 ⊢ a = d → τ ↔ θ
5 on3ind.5 ⊢ b = e → η ↔ τ
6 on3ind.6 ⊢ b = e → ζ ↔ θ
7 on3ind.7 ⊢ c = f → σ ↔ τ
8 on3ind.8 ⊢ a = X → φ ↔ ρ
9 on3ind.9 ⊢ b = Y → ρ ↔ μ
10 on3ind.10 ⊢ c = Z → μ ↔ λ
11 on3ind.i ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ a ∀ e ∈ b ∀ f ∈ c θ ∧ ∀ d ∈ a ∀ e ∈ b χ ∧ ∀ d ∈ a ∀ f ∈ c ζ ∧ ∀ d ∈ a ψ ∧ ∀ e ∈ b ∀ f ∈ c τ ∧ ∀ e ∈ b σ ∧ ∀ f ∈ c η → φ
12 eqid ⊢ x y | x ∈ On × On × On ∧ y ∈ On × On × On ∧ 1 st ⁡ 1 st ⁡ x E 1 st ⁡ 1 st ⁡ y ∨ 1 st ⁡ 1 st ⁡ x = 1 st ⁡ 1 st ⁡ y ∧ 2 nd ⁡ 1 st ⁡ x E 2 nd ⁡ 1 st ⁡ y ∨ 2 nd ⁡ 1 st ⁡ x = 2 nd ⁡ 1 st ⁡ y ∧ 2 nd ⁡ x E 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y = x y | x ∈ On × On × On ∧ y ∈ On × On × On ∧ 1 st ⁡ 1 st ⁡ x E 1 st ⁡ 1 st ⁡ y ∨ 1 st ⁡ 1 st ⁡ x = 1 st ⁡ 1 st ⁡ y ∧ 2 nd ⁡ 1 st ⁡ x E 2 nd ⁡ 1 st ⁡ y ∨ 2 nd ⁡ 1 st ⁡ x = 2 nd ⁡ 1 st ⁡ y ∧ 2 nd ⁡ x E 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
13 onfr ⊢ E Fr On
14 epweon ⊢ E We On
15 weso ⊢ E We On → E Or On
16 sopo ⊢ E Or On → E Po On
17 14 15 16 mp2b ⊢ E Po On
18 epse ⊢ E Se On
19 predon ⊢ a ∈ On → Pred E On a = a
20 19 3ad2ant1 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On a = a
21 predon ⊢ b ∈ On → Pred E On b = b
22 21 3ad2ant2 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On b = b
23 predon ⊢ c ∈ On → Pred E On c = c
24 23 3ad2ant3 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On c = c
25 24 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c θ ↔ ∀ f ∈ c θ
26 22 25 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ↔ ∀ e ∈ b ∀ f ∈ c θ
27 20 26 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ↔ ∀ d ∈ a ∀ e ∈ b ∀ f ∈ c θ
28 22 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b χ ↔ ∀ e ∈ b χ
29 20 28 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b χ ↔ ∀ d ∈ a ∀ e ∈ b χ
30 24 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c ζ ↔ ∀ f ∈ c ζ
31 20 30 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ f ∈ Pred E On c ζ ↔ ∀ d ∈ a ∀ f ∈ c ζ
32 27 29 31 3anbi123d ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ∧ ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b χ ∧ ∀ d ∈ Pred E On a ∀ f ∈ Pred E On c ζ ↔ ∀ d ∈ a ∀ e ∈ b ∀ f ∈ c θ ∧ ∀ d ∈ a ∀ e ∈ b χ ∧ ∀ d ∈ a ∀ f ∈ c ζ
33 20 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ψ ↔ ∀ d ∈ a ψ
34 24 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c τ ↔ ∀ f ∈ c τ
35 22 34 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c τ ↔ ∀ e ∈ b ∀ f ∈ c τ
36 22 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b σ ↔ ∀ e ∈ b σ
37 33 35 36 3anbi123d ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ψ ∧ ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c τ ∧ ∀ e ∈ Pred E On b σ ↔ ∀ d ∈ a ψ ∧ ∀ e ∈ b ∀ f ∈ c τ ∧ ∀ e ∈ b σ
38 24 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c η ↔ ∀ f ∈ c η
39 32 37 38 3anbi123d ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ∧ ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b χ ∧ ∀ d ∈ Pred E On a ∀ f ∈ Pred E On c ζ ∧ ∀ d ∈ Pred E On a ψ ∧ ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c τ ∧ ∀ e ∈ Pred E On b σ ∧ ∀ f ∈ Pred E On c η ↔ ∀ d ∈ a ∀ e ∈ b ∀ f ∈ c θ ∧ ∀ d ∈ a ∀ e ∈ b χ ∧ ∀ d ∈ a ∀ f ∈ c ζ ∧ ∀ d ∈ a ψ ∧ ∀ e ∈ b ∀ f ∈ c τ ∧ ∀ e ∈ b σ ∧ ∀ f ∈ c η
40 39 11 sylbid ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ∧ ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b χ ∧ ∀ d ∈ Pred E On a ∀ f ∈ Pred E On c ζ ∧ ∀ d ∈ Pred E On a ψ ∧ ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c τ ∧ ∀ e ∈ Pred E On b σ ∧ ∀ f ∈ Pred E On c η → φ
41 12 13 17 18 13 17 18 13 17 18 1 2 3 4 5 6 7 8 9 10 40 xpord3ind ⊢ X ∈ On ∧ Y ∈ On ∧ Z ∈ On → λ