Step |
Hyp |
Ref |
Expression |
1 |
|
tfrALT.1 |
⊢ 𝐹 = recs ( 𝐺 ) |
2 |
|
predon |
⊢ ( 𝑥 ∈ On → Pred ( E , On , 𝑥 ) = 𝑥 ) |
3 |
2
|
reseq2d |
⊢ ( 𝑥 ∈ On → ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) = ( 𝐵 ↾ 𝑥 ) ) |
4 |
3
|
fveq2d |
⊢ ( 𝑥 ∈ On → ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) |
5 |
4
|
eqeq2d |
⊢ ( 𝑥 ∈ On → ( ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ↔ ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) ) |
6 |
5
|
ralbiia |
⊢ ( ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) |
7 |
|
epweon |
⊢ E We On |
8 |
|
epse |
⊢ E Se On |
9 |
|
df-recs |
⊢ recs ( 𝐺 ) = wrecs ( E , On , 𝐺 ) |
10 |
1 9
|
eqtri |
⊢ 𝐹 = wrecs ( E , On , 𝐺 ) |
11 |
10
|
wfr3 |
⊢ ( ( ( E We On ∧ E Se On ) ∧ ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ) ) → 𝐹 = 𝐵 ) |
12 |
7 8 11
|
mpanl12 |
⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ Pred ( E , On , 𝑥 ) ) ) ) → 𝐹 = 𝐵 ) |
13 |
6 12
|
sylan2br |
⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐹 = 𝐵 ) |
14 |
13
|
eqcomd |
⊢ ( ( 𝐵 Fn On ∧ ∀ 𝑥 ∈ On ( 𝐵 ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐵 ↾ 𝑥 ) ) ) → 𝐵 = 𝐹 ) |