ssnn0fi - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ssnn0fi		Structured version Unicode version

Theorem ssnn0fi 30775

Description: A subset of the nonnegative integers is finite if and only if there is a nonnegative integer so that all integers greater than this integer are not contained in the subset. (Contributed by AV, 3-Oct-2019.)

**Assertion**
Ref	Expression
ssnn0fi

Distinct variable group:

Proof of Theorem ssnn0fi Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnel 2735	. . . . . . . . . 10
2		n0i 3663	. . . . . . . . . 10
3	1, 2	sylbi 195	. . . . . . . . 9
4	3	con4i 130	. . . . . . . 8
5	4	a1d 25	. . . . . . 7
6	5	ralrimivw 2821	. . . . . 6
7		0nn0 10615	. . . . . . . 8
8	7	a1i 11	. . . . . . 7
9		breq1 4316	. . . . . . . . . 10
10	9	imbi1d 317	. . . . . . . . 9
11	10	ralbidv 2756	. . . . . . . 8
12	11	adantl 466	. . . . . . 7 $/\$
13	8, 12	rspcedv 3098	. . . . . 6
14	6, 13	mpd 15	. . . . 5
15	14	a1d 25	. . . 4
16	15	a1d 25	. . 3
17		ltso 9476	. . . . . . 7
18		id 22	. . . . . . . . 9
19		nn0ssre 10604	. . . . . . . . 9
20	18, 19	syl6ss 3389	. . . . . . . 8
21	20	3anim3i 1175	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
22		fisup2g 7737	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23	17, 21, 22	sylancr 663	. . . . . 6 $/\$ $/\$ $/\$
24		simp3 990	. . . . . . 7 $/\$ $/\$
25		breq2 4317	. . . . . . . . . . . . . . . . . . . 20
26	25	notbid 294	. . . . . . . . . . . . . . . . . . 19
27	26	rspcva 3092	. . . . . . . . . . . . . . . . . 18 $/\$
28		ax-1 6	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
29	28	a1d 25	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
30	27, 29	syl 16	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
31	30	expcom 435	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
32	31	com24 87	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
33	32	imp31 432	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
34	1, 33	syl5bi 217	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
35	34	con4d 105	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
36	35	ralrimiva 2820	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
38	37	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39	38	com12 31	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
40	39	reximdva 2849	. . . . . . 7 $/\$ $/\$ $/\$
41		ssrexv 3438	. . . . . . 7
42	24, 40, 41	sylsyld 56	. . . . . 6 $/\$ $/\$ $/\$
43	23, 42	mpd 15	. . . . 5 $/\$ $/\$
44	43	3exp 1186	. . . 4
45	44	com3l 81	. . 3
46	16, 45	pm2.61ine 2711	. 2
47		fzfi 11815	. . . . 5
48		elfz2nn0 11501	. . . . . . . . . . . . 13 $/\$ $/\$
49	48	notbii 296	. . . . . . . . . . . 12 $/\$ $/\$
50		3ianor 982	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\/$
51		3orass 968	. . . . . . . . . . . 12 $\/$ $\/$ $\/$ $\/$
52	49, 50, 51	3bitri 271	. . . . . . . . . . 11 $\/$ $\/$
53		ssel 3371	. . . . . . . . . . . . . . 15
54	53	adantr 465	. . . . . . . . . . . . . 14 $/\$
55	54	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$
56	55	con3rr3 136	. . . . . . . . . . . 12 $/\$ $/\$
57		notnot 291	. . . . . . . . . . . . . 14
58		pm2.24 109	. . . . . . . . . . . . . . . . . . 19
59	58	adantl 466	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	adantr 465	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
61	60	com12 31	. . . . . . . . . . . . . . . 16 $/\$ $/\$
62	61	a1d 25	. . . . . . . . . . . . . . 15 $/\$ $/\$
63		breq2 4317	. . . . . . . . . . . . . . . . . . . . . 22
64		neleq1 2730	. . . . . . . . . . . . . . . . . . . . . 22
65	63, 64	imbi12d 320	. . . . . . . . . . . . . . . . . . . . 21
66	65	rspcva 3092	. . . . . . . . . . . . . . . . . . . 20 $/\$
67		nn0re 10609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		nn0re 10609	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69		ltnle 9475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
70	67, 68, 69	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
71		df-nel 2623	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
72	71	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
73	70, 72	imbi12d 320	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
74	73	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
75	74	ex 434	. . . . . . . . . . . . . . . . . . . . . . 23
76	75	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
77	76	com12 31	. . . . . . . . . . . . . . . . . . . . 21 $/\$
78	77	adantr 465	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
79	66, 78	mpid 41	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
80	79	ex 434	. . . . . . . . . . . . . . . . . 18 $/\$
81	80	com13 80	. . . . . . . . . . . . . . . . 17 $/\$
82	81	imp 429	. . . . . . . . . . . . . . . 16 $/\$ $/\$
83	82	com13 80	. . . . . . . . . . . . . . 15 $/\$ $/\$
84	62, 83	jaoi 379	. . . . . . . . . . . . . 14 $\/$ $/\$ $/\$
85	57, 84	syl5bir 218	. . . . . . . . . . . . 13 $\/$ $/\$ $/\$
86	85	impcom 430	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$
87	56, 86	jaoi3 961	. . . . . . . . . . 11 $\/$ $\/$ $/\$ $/\$
88	52, 87	sylbi 195	. . . . . . . . . 10 $/\$ $/\$
89	88	com12 31	. . . . . . . . 9 $/\$ $/\$
90	89	con4d 105	. . . . . . . 8 $/\$ $/\$
91	90	imp 429	. . . . . . 7 $/\$ $/\$ $/\$
92	91	ralrimiva 2820	. . . . . 6 $/\$ $/\$
93		dfss3 3367	. . . . . 6
94	92, 93	sylibr 212	. . . . 5 $/\$ $/\$
95		ssfi 7554	. . . . 5 $/\$
96	47, 94, 95	sylancr 663	. . . 4 $/\$ $/\$
97	96	ex 434	. . 3 $/\$
98	97	rexlimdva 2862	. 2
99	46, 98	impbid 191	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965

wceq 1369

wcel 1756

wne 2620

wnel 2621

wral 2736

wrex 2737

wss 3349

c0 3658 class class class wbr 4313

wor 4661 (class class class)co 6112

cfn 7331

cr 9302

cc0 9303

clt 9439

cle 9440

cn0 10600

cfz 11458

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393 ax-cnex 9359 ax-resscn 9360 ax-1cn 9361 ax-icn 9362 ax-addcl 9363 ax-addrcl 9364 ax-mulcl 9365 ax-mulrcl 9366 ax-mulcom 9367 ax-addass 9368 ax-mulass 9369 ax-distr 9370 ax-i2m1 9371 ax-1ne0 9372 ax-1rid 9373 ax-rnegex 9374 ax-rrecex 9375 ax-cnre 9376 ax-pre-lttri 9377 ax-pre-lttrn 9378 ax-pre-ltadd 9379 ax-pre-mulgt0 9380

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-riota 6073 df-ov 6115 df-oprab 6116 df-mpt2 6117 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-1o 6941 df-er 7122 df-en 7332 df-dom 7333 df-sdom 7334 df-fin 7335 df-pnf 9441 df-mnf 9442 df-xr 9443 df-ltxr 9444 df-le 9445 df-sub 9618 df-neg 9619 df-nn 10344 df-n0 10601 df-z 10668 df-uz 10883 df-fz 11459

This theorem is referenced by: rabssnn0fi 30776

W3C validator