ssnn0fi - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ssnn0fi		Structured version Unicode version

Theorem ssnn0fi 12052

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 2807	. . . . . . . . . 10
2		n0i 3785	. . . . . . . . . 10
3	1, 2	sylbi 195	. . . . . . . . 9
4	3	con4i 130	. . . . . . . 8
5	4	a1d 25	. . . . . . 7
6	5	ralrimivw 2874	. . . . . 6
7		0nn0 10801	. . . . . . . 8
8	7	a1i 11	. . . . . . 7
9		breq1 4445	. . . . . . . . . 10
10	9	imbi1d 317	. . . . . . . . 9
11	10	ralbidv 2898	. . . . . . . 8
12	11	adantl 466	. . . . . . 7 $/\$
13	8, 12	rspcedv 3213	. . . . . 6
14	6, 13	mpd 15	. . . . 5
15	14	a1d 25	. . . 4
16	15	a1d 25	. . 3
17		ltso 9656	. . . . . . 7
18		id 22	. . . . . . . . 9
19		nn0ssre 10790	. . . . . . . . 9
20	18, 19	syl6ss 3511	. . . . . . . 8
21	20	3anim3i 1179	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
22		fisup2g 7917	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
23	17, 21, 22	sylancr 663	. . . . . 6 $/\$ $/\$ $/\$
24		simp3 993	. . . . . . 7 $/\$ $/\$
25		breq2 4446	. . . . . . . . . . . . . . . . . . . 20
26	25	notbid 294	. . . . . . . . . . . . . . . . . . 19
27	26	rspcva 3207	. . . . . . . . . . . . . . . . . 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 2873	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
37	36	ex 434	. . . . . . . . . 10 $/\$ $/\$ $/\$
38	37	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
39	38	com12 31	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
40	39	reximdva 2933	. . . . . . 7 $/\$ $/\$ $/\$
41		ssrexv 3560	. . . . . . 7
42	24, 40, 41	sylsyld 56	. . . . . 6 $/\$ $/\$ $/\$
43	23, 42	mpd 15	. . . . 5 $/\$ $/\$
44	43	3exp 1190	. . . 4
45	44	com3l 81	. . 3
46	16, 45	pm2.61ine 2775	. 2
47		fzfi 12040	. . . . 5
48		elfz2nn0 11759	. . . . . . . . . . . . 13 $/\$ $/\$
49	48	notbii 296	. . . . . . . . . . . 12 $/\$ $/\$
50		3ianor 985	. . . . . . . . . . . 12 $/\$ $/\$ $\/$ $\/$
51		3orass 971	. . . . . . . . . . . 12 $\/$ $\/$ $\/$ $\/$
52	49, 50, 51	3bitri 271	. . . . . . . . . . 11 $\/$ $\/$
53		ssel 3493	. . . . . . . . . . . . . . 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 4446	. . . . . . . . . . . . . . . . . . . . . 22
64		neleq1 2800	. . . . . . . . . . . . . . . . . . . . . 22
65	63, 64	imbi12d 320	. . . . . . . . . . . . . . . . . . . . 21
66	65	rspcva 3207	. . . . . . . . . . . . . . . . . . . 20 $/\$
67		nn0re 10795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
68		nn0re 10795	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
69		ltnle 9655	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
70	67, 68, 69	syl2an 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
71		df-nel 2660	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 963	. . . . . . . . . . 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 2873	. . . . . 6 $/\$ $/\$
93		dfss3 3489	. . . . . 6
94	92, 93	sylibr 212	. . . . 5 $/\$ $/\$
95		ssfi 7732	. . . . 5 $/\$
96	47, 94, 95	sylancr 663	. . . 4 $/\$ $/\$
97	96	ex 434	. . 3 $/\$
98	97	rexlimdva 2950	. 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 967 $/\$ w3a 968

wceq 1374

wcel 1762

wne 2657

wnel 2658

wral 2809

wrex 2810

wss 3471

c0 3780 class class class wbr 4442

wor 4794 (class class class)co 6277

cfn 7508

cr 9482

cc0 9483

clt 9619

cle 9620

cn0 10786

cfz 11663

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440 ax-sep 4563 ax-nul 4571 ax-pow 4620 ax-pr 4681 ax-un 6569 ax-cnex 9539 ax-resscn 9540 ax-1cn 9541 ax-icn 9542 ax-addcl 9543 ax-addrcl 9544 ax-mulcl 9545 ax-mulrcl 9546 ax-mulcom 9547 ax-addass 9548 ax-mulass 9549 ax-distr 9550 ax-i2m1 9551 ax-1ne0 9552 ax-1rid 9553 ax-rnegex 9554 ax-rrecex 9555 ax-cnre 9556 ax-pre-lttri 9557 ax-pre-lttrn 9558 ax-pre-ltadd 9559 ax-pre-mulgt0 9560

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2274 df-mo 2275 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-ne 2659 df-nel 2660 df-ral 2814 df-rex 2815 df-reu 2816 df-rmo 2817 df-rab 2818 df-v 3110 df-sbc 3327 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3781 df-if 3935 df-pw 4007 df-sn 4023 df-pr 4025 df-tp 4027 df-op 4029 df-uni 4241 df-iun 4322 df-br 4443 df-opab 4501 df-mpt 4502 df-tr 4536 df-eprel 4786 df-id 4790 df-po 4795 df-so 4796 df-fr 4833 df-we 4835 df-ord 4876 df-on 4877 df-lim 4878 df-suc 4879 df-xp 5000 df-rel 5001 df-cnv 5002 df-co 5003 df-dm 5004 df-rn 5005 df-res 5006 df-ima 5007 df-iota 5544 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6674 df-1st 6776 df-2nd 6777 df-recs 7034 df-rdg 7068 df-1o 7122 df-er 7303 df-en 7509 df-dom 7510 df-sdom 7511 df-fin 7512 df-pnf 9621 df-mnf 9622 df-xr 9623 df-ltxr 9624 df-le 9625 df-sub 9798 df-neg 9799 df-nn 10528 df-n0 10787 df-z 10856 df-uz 11074 df-fz 11664

This theorem is referenced by: rabssnn0fi 12053

W3C validator