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 onfr ⊢ E Fr On
13 epweon ⊢ E We On
14 weso ⊢ E We On → E Or On
15 sopo ⊢ E Or On → E Po On
16 13 14 15 mp2b ⊢ E Po On
17 epse ⊢ E Se On
18 predon ⊢ a ∈ On → Pred E On a = a
19 18 3ad2ant1 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On a = a
20 predon ⊢ b ∈ On → Pred E On b = b
21 20 3ad2ant2 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On b = b
22 predon ⊢ c ∈ On → Pred E On c = c
23 22 3ad2ant3 ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → Pred E On c = c
24 23 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c θ ↔ ∀ f ∈ c θ
25 21 24 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c θ ↔ ∀ e ∈ b ∀ f ∈ c θ
26 19 25 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 θ
27 21 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b χ ↔ ∀ e ∈ b χ
28 19 27 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ e ∈ Pred E On b χ ↔ ∀ d ∈ a ∀ e ∈ b χ
29 23 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c ζ ↔ ∀ f ∈ c ζ
30 19 29 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ∀ f ∈ Pred E On c ζ ↔ ∀ d ∈ a ∀ f ∈ c ζ
31 26 28 30 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 ζ
32 19 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ d ∈ Pred E On a ψ ↔ ∀ d ∈ a ψ
33 23 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c τ ↔ ∀ f ∈ c τ
34 21 33 raleqbidv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b ∀ f ∈ Pred E On c τ ↔ ∀ e ∈ b ∀ f ∈ c τ
35 21 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ e ∈ Pred E On b σ ↔ ∀ e ∈ b σ
36 32 34 35 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 σ
37 23 raleqdv ⊢ a ∈ On ∧ b ∈ On ∧ c ∈ On → ∀ f ∈ Pred E On c η ↔ ∀ f ∈ c η
38 31 36 37 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 η
39 38 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 η → φ
40 12 16 17 12 16 17 12 16 17 1 2 3 4 5 6 7 8 9 10 39 xpord3ind ⊢ X ∈ On ∧ Y ∈ On ∧ Z ∈ On → λ