Step |
Hyp |
Ref |
Expression |
1 |
|
bnj590.1 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
2 |
|
rsp |
⊢ ( ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
3 |
1 2
|
sylbi |
⊢ ( 𝜓 → ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
4 |
|
eleq1 |
⊢ ( 𝐵 = suc 𝑖 → ( 𝐵 ∈ 𝑛 ↔ suc 𝑖 ∈ 𝑛 ) ) |
5 |
|
fveqeq2 |
⊢ ( 𝐵 = suc 𝑖 → ( ( 𝑓 ‘ 𝐵 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
6 |
4 5
|
imbi12d |
⊢ ( 𝐵 = suc 𝑖 → ( ( 𝐵 ∈ 𝑛 → ( 𝑓 ‘ 𝐵 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
7 |
6
|
imbi2d |
⊢ ( 𝐵 = suc 𝑖 → ( ( 𝑖 ∈ ω → ( 𝐵 ∈ 𝑛 → ( 𝑓 ‘ 𝐵 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ↔ ( 𝑖 ∈ ω → ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ) |
8 |
3 7
|
syl5ibr |
⊢ ( 𝐵 = suc 𝑖 → ( 𝜓 → ( 𝑖 ∈ ω → ( 𝐵 ∈ 𝑛 → ( 𝑓 ‘ 𝐵 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) ) |
9 |
8
|
imp |
⊢ ( ( 𝐵 = suc 𝑖 ∧ 𝜓 ) → ( 𝑖 ∈ ω → ( 𝐵 ∈ 𝑛 → ( 𝑓 ‘ 𝐵 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |