Theorem isinf 7787

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 4424	. . . . . 6 |- ( n = (/) -> ( x ~~ n <-> x ~~ (/) ) )
2	1	anbi2d 708	. . . . 5 |- ( n = (/) -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ (/) ) ) )
3	2	exbidv 1758	. . . 4 |- ( n = (/) -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ (/) ) ) )
4		breq2 4424	. . . . . 6 |- ( n = m -> ( x ~~ n <-> x ~~ m ) )
5	4	anbi2d 708	. . . . 5 |- ( n = m -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ m ) ) )
6	5	exbidv 1758	. . . 4 |- ( n = m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ m ) ) )
7		sseq1 3485	. . . . . . 7 |- ( x = y -> ( x C_ A <-> y C_ A ) )
8	7	adantl 467	. . . . . 6 |- ( ( n = suc m /\ x = y ) -> ( x C_ A <-> y C_ A ) )
9		breq1 4423	. . . . . . 7 |- ( x = y -> ( x ~~ n <-> y ~~ n ) )
10		breq2 4424	. . . . . . 7 |- ( n = suc m -> ( y ~~ n <-> y ~~ suc m ) )
11	9, 10	sylan9bbr 705	. . . . . 6 |- ( ( n = suc m /\ x = y ) -> ( x ~~ n <-> y ~~ suc m ) )
12	8, 11	anbi12d 715	. . . . 5 |- ( ( n = suc m /\ x = y ) -> ( ( x C_ A /\ x ~~ n ) <-> ( y C_ A /\ y ~~ suc m ) ) )
13	12	cbvexdva 2086	. . . 4 |- ( n = suc m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. y ( y C_ A /\ y ~~ suc m ) ) )
14		0ss 3791	. . . . . 6 |- (/) C_ A
15		0ex 4552	. . . . . . 7 |- (/) e. _V
16	15	enref 7605	. . . . . 6 |- (/) ~~ (/)
17		sseq1 3485	. . . . . . . 8 |- ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
18		breq1 4423	. . . . . . . 8 |- ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) )
19	17, 18	anbi12d 715	. . . . . . 7 |- ( x = (/) -> ( ( x C_ A /\ x ~~ (/) ) <-> ( (/) C_ A /\ (/) ~~ (/) ) ) )
20	15, 19	spcev 3173	. . . . . 6 |- ( ( (/) C_ A /\ (/) ~~ (/) ) -> E. x ( x C_ A /\ x ~~ (/) ) )
21	14, 16, 20	mp2an 676	. . . . 5 |- E. x ( x C_ A /\ x ~~ (/) )
22	21	a1i 11	. . . 4 |- ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ (/) ) )
23		ssdif0 3851	. . . . . . . . . . . . 13 |- ( A C_ x <-> ( A \ x ) = (/) )
24		eqss 3479	. . . . . . . . . . . . . . 15 |- ( x = A <-> ( x C_ A /\ A C_ x ) )
25		breq1 4423	. . . . . . . . . . . . . . . . . . 19 |- ( x = A -> ( x ~~ m <-> A ~~ m ) )
26	25	biimpa 486	. . . . . . . . . . . . . . . . . 18 |- ( ( x = A /\ x ~~ m ) -> A ~~ m )
27		rspe 2883	. . . . . . . . . . . . . . . . . 18 |- ( ( m e. om /\ A ~~ m ) -> E. m e. om A ~~ m )
28	26, 27	sylan2 476	. . . . . . . . . . . . . . . . 17 |- ( ( m e. om /\ ( x = A /\ x ~~ m ) ) -> E. m e. om A ~~ m )
29		isfi 7596	. . . . . . . . . . . . . . . . 17 |- ( A e. Fin <-> E. m e. om A ~~ m )
30	28, 29	sylibr 215	. . . . . . . . . . . . . . . 16 |- ( ( m e. om /\ ( x = A /\ x ~~ m ) ) -> A e. Fin )
31	30	expcom 436	. . . . . . . . . . . . . . 15 |- ( ( x = A /\ x ~~ m ) -> ( m e. om -> A e. Fin ) )
32	24, 31	sylanbr 475	. . . . . . . . . . . . . 14 |- ( ( ( x C_ A /\ A C_ x ) /\ x ~~ m ) -> ( m e. om -> A e. Fin ) )
33	32	ex 435	. . . . . . . . . . . . 13 |- ( ( x C_ A /\ A C_ x ) -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) )
34	23, 33	sylan2br 478	. . . . . . . . . . . 12 |- ( ( x C_ A /\ ( A \ x ) = (/) ) -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) )
35	34	expcom 436	. . . . . . . . . . 11 |- ( ( A \ x ) = (/) -> ( x C_ A -> ( x ~~ m -> ( m e. om -> A e. Fin ) ) ) )
36	35	3impd 1219	. . . . . . . . . 10 |- ( ( A \ x ) = (/) -> ( ( x C_ A /\ x ~~ m /\ m e. om ) -> A e. Fin ) )
37	36	com12 32	. . . . . . . . 9 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( ( A \ x ) = (/) -> A e. Fin ) )
38	37	con3d 138	. . . . . . . 8 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. A e. Fin -> -. ( A \ x ) = (/) ) )
39		bren 7582	. . . . . . . . . . 11 |- ( x ~~ m <-> E. f f : x -1-1-onto-> m )
40		neq0 3772	. . . . . . . . . . . . . . 15 |- ( -. ( A \ x ) = (/) <-> E. z z e. ( A \ x ) )
41		eldifi 3587	. . . . . . . . . . . . . . . . . . . . . 22 |- ( z e. ( A \ x ) -> z e. A )
42	41	snssd 4142	. . . . . . . . . . . . . . . . . . . . 21 |- ( z e. ( A \ x ) -> { z } C_ A )
43		unss 3640	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( x C_ A /\ { z } C_ A ) <-> ( x u. { z } ) C_ A )
44	43	biimpi 197	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x C_ A /\ { z } C_ A ) -> ( x u. { z } ) C_ A )
45	42, 44	sylan2 476	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x C_ A /\ z e. ( A \ x ) ) -> ( x u. { z } ) C_ A )
46	45	ad2ant2r 751	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) C_ A )
47		vex 3084	. . . . . . . . . . . . . . . . . . . . . . . 24 |- z e. _V
48		vex 3084	. . . . . . . . . . . . . . . . . . . . . . . 24 |- m e. _V
49	47, 48	f1osn 5864	. . . . . . . . . . . . . . . . . . . . . . 23 |- { <. z , m >. } : { z } -1-1-onto-> { m }
50	49	jctr 544	. . . . . . . . . . . . . . . . . . . . . 22 |- ( f : x -1-1-onto-> m -> ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) )
51		eldifn 3588	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. ( A \ x ) -> -. z e. x )
52		disjsn 4057	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( x i^i { z } ) = (/) <-> -. z e. x )
53	51, 52	sylibr 215	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( z e. ( A \ x ) -> ( x i^i { z } ) = (/) )
54		nnord 6710	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( m e. om -> Ord m )
55		orddisj 5476	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( Ord m -> ( m i^i { m } ) = (/) )
56	54, 55	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( m e. om -> ( m i^i { m } ) = (/) )
57	53, 56	anim12i 568	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( z e. ( A \ x ) /\ m e. om ) -> ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) )
58		f1oun 5846	. . . . . . . . . . . . . . . . . . . . . 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 479	. . . . . . . . . . . . . . . . . . . . 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 5444	. . . . . . . . . . . . . . . . . . . . . . 23 |- suc m = ( m u. { m } )
61		f1oeq3 5820	. . . . . . . . . . . . . . . . . . . . . . 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 3084	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- f e. _V
64		snex 4658	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- { <. z , m >. } e. _V
65	63, 64	unex 6599	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( f u. { <. z , m >. } ) e. _V
66		f1oeq1 5818	. . . . . . . . . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . . . . . . . . . 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 7582	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( x u. { z } ) ~~ suc m <-> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
69	67, 68	sylibr 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> ( x u. { z } ) ~~ suc m )
70	62, 69	sylbir 216	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) -> ( x u. { z } ) ~~ suc m )
71	59, 70	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) ~~ suc m )
72	71	adantll 718	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. om ) ) -> ( x u. { z } ) ~~ suc m )
73		vex 3084	. . . . . . . . . . . . . . . . . . . . 21 |- x e. _V
74		snex 4658	. . . . . . . . . . . . . . . . . . . . 21 |- { z } e. _V
75	73, 74	unex 6599	. . . . . . . . . . . . . . . . . . . 20 |- ( x u. { z } ) e. _V
76		sseq1 3485	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x u. { z } ) -> ( y C_ A <-> ( x u. { z } ) C_ A ) )
77		breq1 4423	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = ( x u. { z } ) -> ( y ~~ suc m <-> ( x u. { z } ) ~~ suc m ) )
78	76, 77	anbi12d 715	. . . . . . . . . . . . . . . . . . . 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 3173	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) -> E. y ( y C_ A /\ y ~~ suc m ) )
80	46, 72, 79	syl2anc 665	. . . . . . . . . . . . . . . . . 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 436	. . . . . . . . . . . . . . . . 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 435	. . . . . . . . . . . . . . . 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 1766	. . . . . . . . . . . . . . 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 198	. . . . . . . . . . . . . 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 83	. . . . . . . . . . . . 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 436	. . . . . . . . . . . 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 1766	. . . . . . . . . . 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 198	. . . . . . . . . 10 |- ( x ~~ m -> ( x C_ A -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
89	88	com12 32	. . . . . . . . 9 |- ( x C_ A -> ( x ~~ m -> ( m e. om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
90	89	3imp 1199	. . . . . . . 8 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
91	38, 90	syld 45	. . . . . . 7 |- ( ( x C_ A /\ x ~~ m /\ m e. om ) -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) )
92	91	3expia 1207	. . . . . 6 |- ( ( x C_ A /\ x ~~ m ) -> ( m e. om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
93	92	exlimiv 1766	. . . . 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 84	. . . 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 6731	. . 3 |- ( n e. om -> ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ n ) ) )
96	95	com12 32	. 2 |- ( -. A e. Fin -> ( n e. om -> E. x ( x C_ A /\ x ~~ n ) ) )
97	96	ralrimiv 2837	1 |- ( -. A e. Fin -> A. n e. om E. x ( x C_ A /\ x ~~ n ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1659   e. wcel 1868   A.wral 2775   E.wrex 2776   \ cdif 3433   u. cun 3434   i^i cin 3435   C_ wss 3436   (/)c0 3761   {csn 3996   <.cop 4002   class class class wbr 4420   Ord word 5437   suc csuc 5440   -1-1-onto->wf1o 5596   omcom 6702   ~~ cen 7570   Fincfn 7573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-om 6703  df-en 7574  df-fin 7577

This theorem is referenced by:  fineqvlem  7788  isinffi  8427  domtriomlem  8872  ishashinf  12623