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 |
|
incom |
⊢ ( ( V ∖ Fin ) ∩ Fin ) = ( Fin ∩ ( V ∖ Fin ) ) |
10 |
|
disjdif |
⊢ ( Fin ∩ ( V ∖ Fin ) ) = ∅ |
11 |
9 10
|
eqtri |
⊢ ( ( V ∖ Fin ) ∩ Fin ) = ∅ |
12 |
|
pnfex |
⊢ +∞ ∈ V |
13 |
12
|
fconst |
⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } |
14 |
|
ffn |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } → ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) ) |
15 |
|
fnresdisj |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) → ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) ) |
16 |
13 14 15
|
mp2b |
⊢ ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) |
17 |
11 16
|
mpbi |
⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ |
18 |
8 17
|
uneq12i |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) |
19 |
|
un0 |
⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
20 |
18 19
|
eqtri |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
21 |
2 20
|
eqtri |
⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
22 |
|
df-hash |
⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) |
23 |
22
|
reseq1i |
⊢ ( ♯ ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) |
24 |
1
|
coeq1i |
⊢ ( 𝐺 ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) |
25 |
21 23 24
|
3eqtr4i |
⊢ ( ♯ ↾ Fin ) = ( 𝐺 ∘ card ) |
26 |
25
|
fveq1i |
⊢ ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ( 𝐺 ∘ card ) ‘ 𝐴 ) |
27 |
|
cardf2 |
⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On |
28 |
|
ffun |
⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card ) |
29 |
27 28
|
ax-mp |
⊢ Fun card |
30 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
31 |
|
fvco |
⊢ ( ( Fun card ∧ 𝐴 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
32 |
29 30 31
|
sylancr |
⊢ ( 𝐴 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
33 |
26 32
|
syl5eq |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) ) |
34 |
|
fvres |
⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) ) |
35 |
33 34
|
eqtr3d |
⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) ) |