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 λ