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
|
syl5ibr |
⊢ ( ( 𝜓 ↔ 𝜏 ) → ( 𝑥 = 𝑋 → ( ( 𝜂 → ( 𝑛 ∈ ℕ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 → ( 𝑆 ( 𝑅 ↑𝑟 𝑛 ) 𝑋 → 𝜏 ) ) ) |