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 )