Metamath Proof Explorer

Theorem relexpind

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

Ref Expression
Hypotheses relexpind.1 ⊢ ( 𝜂 → Rel 𝑅 )
relexpind.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
relexpind.3 ⊢ ( 𝜂 → 𝑋 ∈ 𝑊 )
relexpind.4 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
relexpind.5 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
relexpind.6 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
relexpind.7 ⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜏 ) )
relexpind.8 ⊢ ( 𝜂 → 𝜒 )
relexpind.9 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
Assertion relexpind ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) )

Proof

Step Hyp Ref Expression
1 relexpind.1 ⊢ ( 𝜂 → Rel 𝑅 )
2 relexpind.2 ⊢ ( 𝜂 → 𝑆 ∈ 𝑉 )
3 relexpind.3 ⊢ ( 𝜂 → 𝑋 ∈ 𝑊 )
4 relexpind.4 ⊢ ( 𝑖 = 𝑆 → ( 𝜑 ↔ 𝜒 ) )
5 relexpind.5 ⊢ ( 𝑖 = 𝑥 → ( 𝜑 ↔ 𝜓 ) )
6 relexpind.6 ⊢ ( 𝑖 = 𝑗 → ( 𝜑 ↔ 𝜃 ) )
7 relexpind.7 ⊢ ( 𝑥 = 𝑋 → ( 𝜓 ↔ 𝜏 ) )
8 relexpind.8 ⊢ ( 𝜂 → 𝜒 )
9 relexpind.9 ⊢ ( 𝜂 → ( 𝑗 𝑅 𝑥 → ( 𝜃 → 𝜓 ) ) )
10 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 ↔ 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 ) )
11 10 imbi1d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) )
12 11 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) ↔ ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) )
13 12 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) ) )
14 imbi2 ⊢ ( ( 𝜓 ↔ 𝜏 ) → ( ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ↔ ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) )
15 14 imbi2d ⊢ ( ( 𝜓 ↔ 𝜏 ) → ( ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ↔ ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) ) )
16 15 imbi2d ⊢ ( ( 𝜓 ↔ 𝜏 ) → ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) ) ) )
17 16 bibi1d ⊢ ( ( 𝜓 ↔ 𝜏 ) → ( ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) ) ↔ ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜏 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) ) ) )
18 13 17 imbitrrid ⊢ ( ( 𝜓 ↔ 𝜏 ) → ( 𝑥 = 𝑋 → ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) ) ) )
19 7 18 mpcom ⊢ ( 𝑥 = 𝑋 → ( ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) ) ↔ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) ) )
20 1 2 4 5 6 8 9 relexpindlem ⊢ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑥 → 𝜓 ) ) )
21 19 20 vtoclg ⊢ ( 𝑋 ∈ 𝑊 → ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) )
22 3 21 mpcom ⊢ ( 𝜂 → ( 𝑛 ∈ ℕ0 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) )