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 ⊢EFrOn
13 epweon ⊢EWeOn
14 weso ⊢EWeOn→EOrOn
15 sopo ⊢EOrOn→EPoOn
16 13 14 15 mp2b ⊢EPoOn
17 epse ⊢ESeOn
18 predon ⊢a∈On→PredEOna=a
19 18 3ad2ant1 ⊢a∈On∧b∈On∧c∈On→PredEOna=a
20 predon ⊢b∈On→PredEOnb=b
21 20 3ad2ant2 ⊢a∈On∧b∈On∧c∈On→PredEOnb=b
22 predon ⊢c∈On→PredEOnc=c
23 22 3ad2ant3 ⊢a∈On∧b∈On∧c∈On→PredEOnc=c
24 23 raleqdv ⊢a∈On∧b∈On∧c∈On→∀f∈PredEOncθ↔∀f∈cθ
25 21 24 raleqbidv ⊢a∈On∧b∈On∧c∈On→∀e∈PredEOnb∀f∈PredEOncθ↔∀e∈b∀f∈cθ
26 19 25 raleqbidv ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOna∀e∈PredEOnb∀f∈PredEOncθ↔∀d∈a∀e∈b∀f∈cθ
27 21 raleqdv ⊢a∈On∧b∈On∧c∈On→∀e∈PredEOnbχ↔∀e∈bχ
28 19 27 raleqbidv ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOna∀e∈PredEOnbχ↔∀d∈a∀e∈bχ
29 23 raleqdv ⊢a∈On∧b∈On∧c∈On→∀f∈PredEOncζ↔∀f∈cζ
30 19 29 raleqbidv ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOna∀f∈PredEOncζ↔∀d∈a∀f∈cζ
31 26 28 30 3anbi123d ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOna∀e∈PredEOnb∀f∈PredEOncθ∧∀d∈PredEOna∀e∈PredEOnbχ∧∀d∈PredEOna∀f∈PredEOncζ↔∀d∈a∀e∈b∀f∈cθ∧∀d∈a∀e∈bχ∧∀d∈a∀f∈cζ
32 19 raleqdv ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOnaψ↔∀d∈aψ
33 23 raleqdv ⊢a∈On∧b∈On∧c∈On→∀f∈PredEOncτ↔∀f∈cτ
34 21 33 raleqbidv ⊢a∈On∧b∈On∧c∈On→∀e∈PredEOnb∀f∈PredEOncτ↔∀e∈b∀f∈cτ
35 21 raleqdv ⊢a∈On∧b∈On∧c∈On→∀e∈PredEOnbσ↔∀e∈bσ
36 32 34 35 3anbi123d ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOnaψ∧∀e∈PredEOnb∀f∈PredEOncτ∧∀e∈PredEOnbσ↔∀d∈aψ∧∀e∈b∀f∈cτ∧∀e∈bσ
37 23 raleqdv ⊢a∈On∧b∈On∧c∈On→∀f∈PredEOncη↔∀f∈cη
38 31 36 37 3anbi123d ⊢a∈On∧b∈On∧c∈On→∀d∈PredEOna∀e∈PredEOnb∀f∈PredEOncθ∧∀d∈PredEOna∀e∈PredEOnbχ∧∀d∈PredEOna∀f∈PredEOncζ∧∀d∈PredEOnaψ∧∀e∈PredEOnb∀f∈PredEOncτ∧∀e∈PredEOnbσ∧∀f∈PredEOncη↔∀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∈PredEOna∀e∈PredEOnb∀f∈PredEOncθ∧∀d∈PredEOna∀e∈PredEOnbχ∧∀d∈PredEOna∀f∈PredEOncζ∧∀d∈PredEOnaψ∧∀e∈PredEOnb∀f∈PredEOncτ∧∀e∈PredEOnbσ∧∀f∈PredEOncη→φ
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→λ