Metamath Proof Explorer


Theorem hashgval

Description: The value of the # function in terms of the mapping G from _om to NN0 . The proof avoids the use of ax-ac . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 26-Dec-2014)

Ref Expression
Hypothesis hashgval.1 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion hashgval ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Proof

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 ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )