Step |
Hyp |
Ref |
Expression |
1 |
|
hashgval.1 |
⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) |
2 |
|
resundir |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) |
3 |
|
eqid |
⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) |
4 |
|
eqid |
⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
5 |
3 4
|
hashkf |
⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0 |
6 |
|
ffn |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin ) |
7 |
|
fnresdm |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ) |
8 |
5 6 7
|
mp2b |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
9 |
|
disjdifr |
⊢ ( ( V ∖ Fin ) ∩ Fin ) = ∅ |
10 |
|
pnfex |
⊢ +∞ ∈ V |
11 |
10
|
fconst |
⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } |
12 |
|
ffn |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } → ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) ) |
13 |
|
fnresdisj |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) → ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) ) |
14 |
11 12 13
|
mp2b |
⊢ ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) |
15 |
9 14
|
mpbi |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ |
16 |
8 15
|
uneq12i |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) |
17 |
|
un0 |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
18 |
16 17
|
eqtri |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
19 |
2 18
|
eqtri |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
20 |
|
df-hash |
⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) |
21 |
20
|
reseq1i |
⊢ ( ♯ ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) |
22 |
1
|
coeq1i |
⊢ ( 𝐺 ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
23 |
19 21 22
|
3eqtr4i |
⊢ ( ♯ ↾ Fin ) = ( 𝐺 ∘ card ) |
24 |
23
|
fveq1i |
⊢ ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ( 𝐺 ∘ card ) ‘ 𝐴 ) |
25 |
|
cardf2 |
⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On |
26 |
|
ffun |
⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card ) |
27 |
25 26
|
ax-mp |
⊢ Fun card |
28 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
29 |
|
fvco |
⊢ ( ( Fun card ∧ 𝐴 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
30 |
27 28 29
|
sylancr |
⊢ ( 𝐴 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
31 |
24 30
|
eqtrid |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
32 |
|
fvres |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) |
33 |
31 32
|
eqtr3d |
⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) ) |