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 
|- ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 eldif 
 |-  ( A e. ( _V \ Fin ) <-> ( A e. _V /\ -. A e. Fin ) )
3 df-hash 
 |-  # = ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) )
4 3 reseq1i 
 |-  ( # |` ( _V \ Fin ) ) = ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` ( _V \ Fin ) )
5 resundir 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) u. ( ( _V \ Fin ) X. { +oo } ) ) |` ( _V \ Fin ) ) = ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` ( _V \ Fin ) ) )
6 disjdif 
 |-  ( Fin i^i ( _V \ Fin ) ) = (/)
7 eqid 
 |-  ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
8 eqid 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) = ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card )
9 7 8 hashkf 
 |-  ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0
10 ffn 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) : Fin --> NN0 -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) Fn Fin )
11 fnresdisj 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) Fn Fin -> ( ( Fin i^i ( _V \ Fin ) ) = (/) <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) = (/) ) )
12 9 10 11 mp2b 
 |-  ( ( Fin i^i ( _V \ Fin ) ) = (/) <-> ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) = (/) )
13 6 12 mpbi 
 |-  ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) = (/)
14 pnfex 
 |-  +oo e. _V
15 14 fconst 
 |-  ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo }
16 ffn 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) : ( _V \ Fin ) --> { +oo } -> ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) )
17 fnresdm 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) Fn ( _V \ Fin ) -> ( ( ( _V \ Fin ) X. { +oo } ) |` ( _V \ Fin ) ) = ( ( _V \ Fin ) X. { +oo } ) )
18 15 16 17 mp2b 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) |` ( _V \ Fin ) ) = ( ( _V \ Fin ) X. { +oo } )
19 13 18 uneq12i 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` ( _V \ Fin ) ) ) = ( (/) u. ( ( _V \ Fin ) X. { +oo } ) )
20 uncom 
 |-  ( (/) u. ( ( _V \ Fin ) X. { +oo } ) ) = ( ( ( _V \ Fin ) X. { +oo } ) u. (/) )
21 un0 
 |-  ( ( ( _V \ Fin ) X. { +oo } ) u. (/) ) = ( ( _V \ Fin ) X. { +oo } )
22 19 20 21 3eqtri 
 |-  ( ( ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om ) o. card ) |` ( _V \ Fin ) ) u. ( ( ( _V \ Fin ) X. { +oo } ) |` ( _V \ Fin ) ) ) = ( ( _V \ Fin ) X. { +oo } )
23 4 5 22 3eqtri 
 |-  ( # |` ( _V \ Fin ) ) = ( ( _V \ Fin ) X. { +oo } )
24 23 fveq1i 
 |-  ( ( # |` ( _V \ Fin ) ) ` A ) = ( ( ( _V \ Fin ) X. { +oo } ) ` A )
25 fvres 
 |-  ( A e. ( _V \ Fin ) -> ( ( # |` ( _V \ Fin ) ) ` A ) = ( # ` A ) )
26 14 fvconst2 
 |-  ( A e. ( _V \ Fin ) -> ( ( ( _V \ Fin ) X. { +oo } ) ` A ) = +oo )
27 24 25 26 3eqtr3a 
 |-  ( A e. ( _V \ Fin ) -> ( # ` A ) = +oo )
28 2 27 sylbir 
 |-  ( ( A e. _V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
29 1 28 sylan 
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )