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
|
syl5ibr |
⊢ ( ( t* ‘ 𝑅 ) = ( t*rec ‘ 𝑅 ) → ( 𝜂 → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) ) ) |
27 |
10 26
|
mpcom |
⊢ ( 𝜂 → ( 𝑆 ( t* ‘ 𝑅 ) 𝑋 → 𝜏 ) ) |