This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ishashinf

Description: Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf . (Contributed by Thierry Arnoux, 5-Jul-2017)

Ref Expression
Assertion ishashinf 
|- ( -. A e. Fin -> A. n e. NN E. x e. ~P A ( # ` x ) = n )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( n e. NN -> ( 1 ... n ) e. Fin )
2 ficardom 
 |-  ( ( 1 ... n ) e. Fin -> ( card ` ( 1 ... n ) ) e. _om )
3 1 2 syl 
 |-  ( n e. NN -> ( card ` ( 1 ... n ) ) e. _om )
4 isinf 
 |-  ( -. A e. Fin -> A. a e. _om E. x ( x C_ A /\ x ~~ a ) )
5 breq2 
 |-  ( a = ( card ` ( 1 ... n ) ) -> ( x ~~ a <-> x ~~ ( card ` ( 1 ... n ) ) ) )
6 5 anbi2d 
 |-  ( a = ( card ` ( 1 ... n ) ) -> ( ( x C_ A /\ x ~~ a ) <-> ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) ) )
7 6 exbidv 
 |-  ( a = ( card ` ( 1 ... n ) ) -> ( E. x ( x C_ A /\ x ~~ a ) <-> E. x ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) ) )
8 7 rspcva 
 |-  ( ( ( card ` ( 1 ... n ) ) e. _om /\ A. a e. _om E. x ( x C_ A /\ x ~~ a ) ) -> E. x ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) )
9 3 4 8 syl2anr 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> E. x ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) )
10 velpw 
 |-  ( x e. ~P A <-> x C_ A )
11 10 biimpri 
 |-  ( x C_ A -> x e. ~P A )
12 11 a1i 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> ( x C_ A -> x e. ~P A ) )
13 hasheni 
 |-  ( x ~~ ( card ` ( 1 ... n ) ) -> ( # ` x ) = ( # ` ( card ` ( 1 ... n ) ) ) )
14 13 adantl 
 |-  ( ( ( -. A e. Fin /\ n e. NN ) /\ x ~~ ( card ` ( 1 ... n ) ) ) -> ( # ` x ) = ( # ` ( card ` ( 1 ... n ) ) ) )
15 hashcard 
 |-  ( ( 1 ... n ) e. Fin -> ( # ` ( card ` ( 1 ... n ) ) ) = ( # ` ( 1 ... n ) ) )
16 1 15 syl 
 |-  ( n e. NN -> ( # ` ( card ` ( 1 ... n ) ) ) = ( # ` ( 1 ... n ) ) )
17 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
18 hashfz1 
 |-  ( n e. NN0 -> ( # ` ( 1 ... n ) ) = n )
19 17 18 syl 
 |-  ( n e. NN -> ( # ` ( 1 ... n ) ) = n )
20 16 19 eqtrd 
 |-  ( n e. NN -> ( # ` ( card ` ( 1 ... n ) ) ) = n )
21 20 ad2antlr 
 |-  ( ( ( -. A e. Fin /\ n e. NN ) /\ x ~~ ( card ` ( 1 ... n ) ) ) -> ( # ` ( card ` ( 1 ... n ) ) ) = n )
22 14 21 eqtrd 
 |-  ( ( ( -. A e. Fin /\ n e. NN ) /\ x ~~ ( card ` ( 1 ... n ) ) ) -> ( # ` x ) = n )
23 22 ex 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> ( x ~~ ( card ` ( 1 ... n ) ) -> ( # ` x ) = n ) )
24 12 23 anim12d 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> ( ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) -> ( x e. ~P A /\ ( # ` x ) = n ) ) )
25 24 eximdv 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> ( E. x ( x C_ A /\ x ~~ ( card ` ( 1 ... n ) ) ) -> E. x ( x e. ~P A /\ ( # ` x ) = n ) ) )
26 9 25 mpd 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> E. x ( x e. ~P A /\ ( # ` x ) = n ) )
27 df-rex 
 |-  ( E. x e. ~P A ( # ` x ) = n <-> E. x ( x e. ~P A /\ ( # ` x ) = n ) )
28 26 27 sylibr 
 |-  ( ( -. A e. Fin /\ n e. NN ) -> E. x e. ~P A ( # ` x ) = n )
29 28 ralrimiva 
 |-  ( -. A e. Fin -> A. n e. NN E. x e. ~P A ( # ` x ) = n )