Step |
Hyp |
Ref |
Expression |
1 |
|
bnj1529.1 |
⊢ ( 𝜒 → ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ) |
2 |
|
bnj1529.2 |
⊢ ( 𝑤 ∈ 𝐹 → ∀ 𝑥 𝑤 ∈ 𝐹 ) |
3 |
|
nfv |
⊢ Ⅎ 𝑦 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) |
4 |
2
|
nfcii |
⊢ Ⅎ 𝑥 𝐹 |
5 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑦 |
6 |
4 5
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) |
7 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐺 |
8 |
|
nfcv |
⊢ Ⅎ 𝑥 pred ( 𝑦 , 𝐴 , 𝑅 ) |
9 |
4 8
|
nfres |
⊢ Ⅎ 𝑥 ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
10 |
5 9
|
nfop |
⊢ Ⅎ 𝑥 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 |
11 |
7 10
|
nffv |
⊢ Ⅎ 𝑥 ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) |
12 |
6 11
|
nfeq |
⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) |
13 |
|
fveq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) |
14 |
|
id |
⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 ) |
15 |
|
bnj602 |
⊢ ( 𝑥 = 𝑦 → pred ( 𝑥 , 𝐴 , 𝑅 ) = pred ( 𝑦 , 𝐴 , 𝑅 ) ) |
16 |
15
|
reseq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) = ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) |
17 |
14 16
|
opeq12d |
⊢ ( 𝑥 = 𝑦 → 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 = 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) |
18 |
17
|
fveq2d |
⊢ ( 𝑥 = 𝑦 → ( 𝐺 ‘ 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) = ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) ) |
19 |
13 18
|
eqeq12d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) ) ) |
20 |
3 12 19
|
cbvralw |
⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 〈 𝑥 , ( 𝐹 ↾ pred ( 𝑥 , 𝐴 , 𝑅 ) ) 〉 ) ↔ ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) ) |
21 |
1 20
|
sylib |
⊢ ( 𝜒 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 〈 𝑦 , ( 𝐹 ↾ pred ( 𝑦 , 𝐴 , 𝑅 ) ) 〉 ) ) |