Metamath Proof Explorer

Theorem hashinf

Description: The value of the # function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014)

Ref Expression
Assertion hashinf ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
2 eldif ⊢ ( 𝐴 ∈ ( V ∖ Fin ) ↔ ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) )
3 df-hash ⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )
4 3 reseq1i ⊢ ( ♯ ↾ ( V ∖ Fin ) ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ ( V ∖ Fin ) )
5 resundir ⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ ( V ∖ Fin ) ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ ( V ∖ Fin ) ) )
6 disjdif ⊢ ( Fin ∩ ( V ∖ Fin ) ) = ∅
7 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
8 eqid ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
9 7 8 hashkf ⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0
10 ffn ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ0 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin )
11 fnresdisj ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin → ( ( Fin ∩ ( V ∖ Fin ) ) = ∅ ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) = ∅ ) )
12 9 10 11 mp2b ⊢ ( ( Fin ∩ ( V ∖ Fin ) ) = ∅ ↔ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) = ∅ )
13 6 12 mpbi ⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) = ∅
14 pnfex ⊢ +∞ ∈ V
15 14 fconst ⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ }
16 ffn ⊢ ( ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } → ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) )
17 fnresdm ⊢ ( ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) → ( ( ( V ∖ Fin ) × { +∞ } ) ↾ ( V ∖ Fin ) ) = ( ( V ∖ Fin ) × { +∞ } ) )
18 15 16 17 mp2b ⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ ( V ∖ Fin ) ) = ( ( V ∖ Fin ) × { +∞ } )
19 13 18 uneq12i ⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ ( V ∖ Fin ) ) ) = ( ∅ ∪ ( ( V ∖ Fin ) × { +∞ } ) )
20 uncom ⊢ ( ∅ ∪ ( ( V ∖ Fin ) × { +∞ } ) ) = ( ( ( V ∖ Fin ) × { +∞ } ) ∪ ∅ )
21 un0 ⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ∪ ∅ ) = ( ( V ∖ Fin ) × { +∞ } )
22 19 20 21 3eqtri ⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ ( V ∖ Fin ) ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ ( V ∖ Fin ) ) ) = ( ( V ∖ Fin ) × { +∞ } )
23 4 5 22 3eqtri ⊢ ( ♯ ↾ ( V ∖ Fin ) ) = ( ( V ∖ Fin ) × { +∞ } )
24 23 fveq1i ⊢ ( ( ♯ ↾ ( V ∖ Fin ) ) ‘ 𝐴 ) = ( ( ( V ∖ Fin ) × { +∞ } ) ‘ 𝐴 )
25 fvres ⊢ ( 𝐴 ∈ ( V ∖ Fin ) → ( ( ♯ ↾ ( V ∖ Fin ) ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
26 14 fvconst2 ⊢ ( 𝐴 ∈ ( V ∖ Fin ) → ( ( ( V ∖ Fin ) × { +∞ } ) ‘ 𝐴 ) = +∞ )
27 24 25 26 3eqtr3a ⊢ ( 𝐴 ∈ ( V ∖ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
28 2 27 sylbir ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )
29 1 28 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ¬ 𝐴 ∈ Fin ) → ( ♯ ‘ 𝐴 ) = +∞ )