Theorem isinf 7752

Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set has countably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013.)

Assertion

Ref	Expression
isinf	|- ( -. A e. Fin -> A. n e. om E. x ( x C_ A /\ x ~~ n ) )

Distinct variable group:   x, A, n

Proof of Theorem isinf

Dummy variables f m y z g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 4460	. . . . . 6 |- ( n = (/) -> ( x ~~ n <-> x ~~ (/) ) )
2	1	anbi2d 703	. . . . 5 |- ( n = (/) -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ (/) ) ) )
3	2	exbidv 1715	. . . 4 |- ( n = (/) -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ (/) ) ) )
4		breq2 4460	. . . . . 6 |- ( n = m -> ( x ~~ n <-> x ~~ m ) )
5	4	anbi2d 703	. . . . 5 |- ( n = m -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ m ) ) )
6	5	exbidv 1715	. . . 4 |- ( n = m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ m ) ) )
7		sseq1 3520	. . . . . . 7 |- ( x = y -> ( x C_ A <-> y C_ A ) )
8	7	adantl 466	. . . . . 6 |- ( ( n = suc m /\ x = y ) -> ( x C_ A <-> y C_ A ) )
9		breq1 4459	. . . . . . 7 |- ( x = y -> ( x ~~ n <-> y ~~ n ) )
10		breq2 4460	. . . . . . 7 |- ( n = suc m -> ( y ~~ n <-> y ~~ suc m ) )
11	9, 10	sylan9bbr 700	. . . . . 6 |- ( ( n = suc m /\ x = y ) -> ( x ~~ n <-> y ~~ suc m ) )
12	8, 11	anbi12d 710	. . . . 5 |- ( ( n = suc m /\ x = y ) -> ( ( x C_ A /\ x ~~ n ) <-> ( y C_ A /\ y ~~ suc m ) ) )
13	12	cbvexdva 2034	. . . 4 |- ( n = suc m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. y ( y C_ A /\ y ~~ suc m ) ) )
14		0ss 3823	. . . . . 6 |- (/) C_ A
15		0ex 4587	. . . . . . 7 |- (/) e. _V
16	15	enref 7567	. . . . . 6 |- (/) ~~ (/)
17		sseq1 3520	. . . . . . . 8 |- ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
18		breq1 4459	. . . . . . . 8 |- ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) )
19	17, 18	anbi12d 710	. . . . . . 7 |- ( x = (/) -> ( ( x C_ A /\ x ~~ (/) ) <-> ( (/) C_ A /\ (/) ~~ (/) ) ) )
20	15, 19	spcev 3201	. . . . . 6 |- ( ( (/) C_ A /\ (/) ~~ (/) ) -> E. x ( x C_ A /\ x ~~ (/) ) )
21	14, 16, 20	mp2an 672	. . . . 5 |- E. x ( x C_ A /\ x ~~ (/) )
22	21	a1i 11	. . . 4 |- ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ (/) ) )
23		ssdif0 3888	. . . . . . . . . . . . 13 |- ( A C_ x <-> ( A \ x ) = (/) )
24		eqss 3514	. . . . . . . . . . . . . . 15 |- ( x = A <-> ( x C_ A /\ A C_ x ) )
25		breq1 4459	. . . . . . . . . . . . . . . . . . 19 |- ( x = A -> ( x ~~ m <-> A ~~ m ) )
26	25	biimpa 484	. . . . . . . . . . . . . . . . . 18 |- ( ( x = A /\ x ~~ m ) -> A ~~ m )
27		rspe 2915	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. om /\ A ~~ m ) -> E. m e. om A ~~ m )
28	26, 27	sylan2 474	. . . . . . . . . . . . . . . . 17 |- ( ( m e. om /\ ( x = A /\ x ~~ m ) ) -> E. m e. om A ~~ m )
29		isfi 7558	. . . . . . . . . . . . . . . . 17 |- ( A e. Fin <-> E. m e. om A ~~ m )
30	28, 29	sylibr 212	. . . . . . . . . . . . . . . 16 |- ( ( m e. om /\ ( x = A /\ x ~~ m ) ) -> A e. Fin )
31	30	expcom 435	. . . . . . . . . . . . . . 15 |- ( ( x = A /\ x ~~ m ) -> ( m e. om -> A e. Fin ) )
32	24, 31	sylanbr 473	. . . . . . . . . . . . . 14 |- ( ( ( x C_ A /\ A C_ x ) /\ x ~~ m ) -> ( m e. om -> A e. Fin ) )
33	32	ex 434	. . . . . . . . . . . . 13 |- ( ( x C_ A /\ A C_ x ) -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) )
34	23, 33	sylan2br 476	. . . . . . . . . . . 12 |- ( ( x C_ A /\ ( A \ x ) = (/) ) -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) )
35	34	expcom 435	. . . . . . . . . . 11 |- ( ( A \ x ) = (/) -> ( x C_ A -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) ) )
36	35	3impd 1210	. . . . . . . . . 10 |- ( ( A \ x ) = (/) -> ( ( x C_ A /\ x ~~ m /\ m e. om ) -> A e. Fin ) )
37	36	com12 31	. . . . . . . . 9 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( ( A \ x ) = (/) -> A e. Fin ) )
38	37	con3d 133	. . . . . . . 8 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. A e. Fin -> -. ( A \ x ) = (/) ) )
39		bren 7544	. . . . . . . . . . 11 |- ( x ~~ m <-> E. f f : x -1-1-onto-> m )
40		neq0 3804	. . . . . . . . . . . . . . 15 |- ( -. ( A \ x ) = (/) <-> E. z z e. ( A \ x ) )
41		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( A \ x ) -> z e. A )
42	41	snssd 4177	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( A \ x ) -> { z } C_ A )
43		unss 3674	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x C_ A /\ { z } C_ A ) <-> ( x u. { z } ) C_ A )
44	43	biimpi 194	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x C_ A /\ { z } C_ A ) -> ( x u. { z } ) C_ A )
45	42, 44	sylan2 474	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x C_ A /\ z e. ( A \ x ) ) -> ( x u. { z } ) C_ A )
46	45	ad2ant2r 746	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) C_ A )
47		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. _V
48		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . 24 |- m e. _V
49	47, 48	f1osn 5859	. . . . . . . . . . . . . . . . . . . . . . 23 |- { <. z , m >. } : { z } -1-1-onto-> { m }
50	49	jctr 542	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : x -1-1-onto-> m -> ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) )
51		eldifn 3623	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( A \ x ) -> -. z e. x )
52		disjsn 4092	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x i^i { z } ) = (/) <-> -. z e. x )
53	51, 52	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. ( A \ x ) -> ( x i^i { z } ) = (/) )
54		nnord 6707	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. om -> Ord m )
55		orddisj 4925	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Ord m -> ( m i^i { m } ) = (/) )
56	54, 55	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( m e. om -> ( m i^i { m } ) = (/) )
57	53, 56	anim12i 566	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ( A \ x ) /\ m e. om ) -> ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) )
58		f1oun 5841	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) /\ ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
59	50, 57, 58	syl2an 477	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
60		df-suc 4893	. . . . . . . . . . . . . . . . . . . . . . 23 |- suc m = ( m u. { m } )
61		f1oeq3 5815	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( suc m = ( m u. { m } ) -> ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) ) )
62	60, 61	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
63		vex 3112	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. _V
64		snex 4697	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- { <. z , m >. } e. _V
65	63, 64	unex 6597	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f u. { <. z , m >. } ) e. _V
66		f1oeq1 5813	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( g = ( f u. { <. z , m >. } ) -> ( g : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m ) )
67	65, 66	spcev 3201	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
68		bren 7544	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x u. { z } ) ~~ suc m <-> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
69	67, 68	sylibr 212	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> ( x u. { z } ) ~~ suc m )
70	62, 69	sylbir 213	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) -> ( x u. { z } ) ~~ suc m )
71	59, 70	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) ~~ suc m )
72	71	adantll 713	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) ~~ suc m )
73		vex 3112	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
74		snex 4697	. . . . . . . . . . . . . . . . . . . . 21 |- { z } e. _V
75	73, 74	unex 6597	. . . . . . . . . . . . . . . . . . . 20 |- ( x u. { z } ) e. _V
76		sseq1 3520	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x u. { z } ) -> ( y C_ A <-> ( x u. { z } ) C_ A ) )
77		breq1 4459	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x u. { z } ) -> ( y ~~ suc m <-> ( x u. { z } ) ~~ suc m ) )
78	76, 77	anbi12d 710	. . . . . . . . . . . . . . . . . . . 20 |- ( y = ( x u. { z } ) -> ( ( y C_ A /\ y ~~ suc m ) <-> ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) ) )
79	75, 78	spcev 3201	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) -> E. y ( y C_ A /\ y ~~ suc m ) )
80	46, 72, 79	syl2anc 661	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. om ) ) -> E. y ( y C_ A /\ y ~~ suc m ) )
81	80	expcom 435	. . . . . . . . . . . . . . . . 17 |- ( ( z e. ( A \ x ) /\ m e. om ) -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
82	81	ex 434	. . . . . . . . . . . . . . . 16 |- ( z e. ( A \ x ) -> ( m e. om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
83	82	exlimiv 1723	. . . . . . . . . . . . . . 15 |- ( E. z z e. ( A \ x ) -> ( m e. om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
84	40, 83	sylbi 195	. . . . . . . . . . . . . 14 |- ( -. ( A \ x ) = (/) -> ( m e. om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
85	84	com13 80	. . . . . . . . . . . . 13 |- ( ( x C_ A /\ f : x -1-1-onto-> m ) -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
86	85	expcom 435	. . . . . . . . . . . 12 |- ( f : x -1-1-onto-> m -> ( x C_ A -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
87	86	exlimiv 1723	. . . . . . . . . . 11 |- ( E. f f : x -1-1-onto-> m -> ( x C_ A -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
88	39, 87	sylbi 195	. . . . . . . . . 10 |- ( x ~~ m -> ( x C_ A -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
89	88	com12 31	. . . . . . . . 9 |- ( x C_ A -> ( x ~~ m -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
90	89	3imp 1190	. . . . . . . 8 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
91	38, 90	syld 44	. . . . . . 7 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) )
92	91	3expia 1198	. . . . . 6 |- ( ( x C_ A /\ x ~~ m ) -> ( m e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
93	92	exlimiv 1723	. . . . 5 |- ( E. x ( x C_ A /\ x ~~ m ) -> ( m e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
94	93	com3l 81	. . . 4 |- ( m e. om -> ( -. A e. Fin -> ( E. x ( x C_ A /\ x ~~ m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
95	3, 6, 13, 22, 94	finds2 6727	. . 3 |- ( n e. om -> ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ n ) ) )
96	95	com12 31	. 2 |- ( -. A e. Fin -> ( n e. om -> E. x ( x C_ A /\ x ~~ n ) ) )
97	96	ralrimiv 2869	1 |- ( -. A e. Fin -> A. n e. om E. x ( x C_ A /\ x ~~ n ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 973   = wceq 1395   E.wex 1613   e. wcel 1819   A.wral 2807   E.wrex 2808   \ cdif 3468   u. cun 3469   i^i cin 3470   C_ wss 3471   (/)c0 3793   {csn 4032   <.cop 4038   class class class wbr 4456   Ord word 4886   suc csuc 4889   -1-1-onto->wf1o 5593   omcom 6699   ~~ cen 7532   Fincfn 7535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-om 6700  df-en 7536  df-fin 7539

This theorem is referenced by:  fineqvlem  7753  isinffi  8390  domtriomlem  8839  ishashinf  27766