Step |
Hyp |
Ref |
Expression |
1 |
|
bnj540.1 |
⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
2 |
|
bnj540.2 |
⊢ ( 𝜓″ ↔ [ 𝐺 / 𝑓 ] 𝜓 ) |
3 |
|
bnj540.3 |
⊢ 𝐺 ∈ V |
4 |
1
|
sbcbii |
⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
5 |
3
|
bnj538 |
⊢ ( [ 𝐺 / 𝑓 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
6 |
|
sbcimg |
⊢ ( 𝐺 ∈ V → ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) ) |
7 |
3 6
|
ax-mp |
⊢ ( [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
8 |
7
|
ralbii |
⊢ ( ∀ 𝑖 ∈ ω [ 𝐺 / 𝑓 ] ( suc 𝑖 ∈ 𝑁 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
9 |
4 5 8
|
3bitri |
⊢ ( [ 𝐺 / 𝑓 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
10 |
3
|
bnj525 |
⊢ ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 ↔ suc 𝑖 ∈ 𝑁 ) |
11 |
|
fveq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ suc 𝑖 ) = ( 𝐺 ‘ suc 𝑖 ) ) |
12 |
|
fveq1 |
⊢ ( 𝑓 = 𝐺 → ( 𝑓 ‘ 𝑖 ) = ( 𝐺 ‘ 𝑖 ) ) |
13 |
12
|
bnj1113 |
⊢ ( 𝑓 = 𝐺 → ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
14 |
11 13
|
eqeq12d |
⊢ ( 𝑓 = 𝐺 → ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
15 |
3 14
|
sbcie |
⊢ ( [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
16 |
10 15
|
imbi12i |
⊢ ( ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
17 |
16
|
ralbii |
⊢ ( ∀ 𝑖 ∈ ω ( [ 𝐺 / 𝑓 ] suc 𝑖 ∈ 𝑁 → [ 𝐺 / 𝑓 ] ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
18 |
2 9 17
|
3bitri |
⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑁 → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |