Metamath Proof Explorer

Theorem rtrclind

Description: Principle of transitive induction. The first three hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015) (Revised by AV, 13-Jul-2024)

Ref Expression
Hypotheses rtrclind.1 ⊢ ( 𝜂 → Rel 𝑅 )
rtrclind.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
rtrclind.3 ⊢ ( 𝜂 → 𝑋 ∈ 𝑊 )
rtrclind.4 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
rtrclind.5 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
rtrclind.6 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
rtrclind.7 ⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜏 ) )
rtrclind.8 ⊢ ( 𝜂 → 𝜒 )
rtrclind.9 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
Assertion rtrclind ( 𝜂 → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) )

Proof

Step Hyp Ref Expression
1 rtrclind.1 ⊢ ( 𝜂 → Rel 𝑅 )
2 rtrclind.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
3 rtrclind.3 ⊢ ( 𝜂 → 𝑋 ∈ 𝑊 )
4 rtrclind.4 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
5 rtrclind.5 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
6 rtrclind.6 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
7 rtrclind.7 ⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜏 ) )
8 rtrclind.8 ⊢ ( 𝜂 → 𝜒 )
9 rtrclind.9 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
10 1 dfrtrcl2 ⊢ ( 𝜂 → ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) )
11 1 dfrtrclrec2 ⊢ ( 𝜂 → ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ↔ ∃ 𝑛 ∈ ℕ0 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ) )
12 11 biimpac ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) → ∃ 𝑛 ∈ ℕ0 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 )
13 simprl ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ ( 𝜂 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) ) → 𝜂 )
14 simprrr ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ ( 𝜂 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) ) → 𝑛 ∈ ℕ0 )
15 simprrl ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ ( 𝜂 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) ) → 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 )
16 1 2 3 4 5 6 7 8 9 relexpind ⊢ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) )
17 13 14 15 16 syl3c ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ ( 𝜂 ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) ) → 𝜏 )
18 17 anassrs ⊢ ( ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) ∧ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) ) → 𝜏 )
19 18 expcom ⊢ ( ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) → 𝜏 ) )
20 19 expcom ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) → 𝜏 ) ) )
21 20 rexlimiv ⊢ ( ∃ 𝑛 ∈ ℕ0 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) → 𝜏 ) )
22 12 21 mpcom ⊢ ( ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ∧ 𝜂 ) → 𝜏 )
23 22 expcom ⊢ ( 𝜂 → ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 → 𝜏 ) )
24 breq ⊢ ( ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 ↔ 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 ) )
25 24 imbi1d ⊢ ( ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) → ( ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) ↔ ( 𝑆 ( t*rec ‘ 𝑅 ) 𝑋 → 𝜏 ) ) )
26 23 25 imbitrrid ⊢ ( ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) → ( 𝜂 → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) ) )
27 10 26 mpcom ⊢ ( 𝜂 → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) )