ssnn0fi - Metamath Proof Explorer

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

Theorem ssnn0fi 12235

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		0nn0 10908	. . . . . 6
2	1	a1i 11	. . . . 5
3		breq1 4398	. . . . . . . 8
4	3	imbi1d 324	. . . . . . 7
5	4	ralbidv 2829	. . . . . 6
6	5	adantl 473	. . . . 5 $/\$
7		nnel 2752	. . . . . . . . 9
8		n0i 3727	. . . . . . . . 9
9	7, 8	sylbi 200	. . . . . . . 8
10	9	con4i 135	. . . . . . 7
11	10	a1d 25	. . . . . 6
12	11	ralrimivw 2810	. . . . 5
13	2, 6, 12	rspcedvd 3143	. . . 4
14	13	2a1d 26	. . 3
15		ltso 9732	. . . . . . 7
16		id 22	. . . . . . . . 9
17		nn0ssre 10897	. . . . . . . . 9
18	16, 17	syl6ss 3430	. . . . . . . 8
19	18	3anim3i 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
20		fisup2g 8002	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
21	15, 19, 20	sylancr 676	. . . . . 6 $/\$ $/\$ $/\$
22		simp3 1032	. . . . . . 7 $/\$ $/\$
23		breq2 4399	. . . . . . . . . . . . . . . . . . . 20
24	23	notbid 301	. . . . . . . . . . . . . . . . . . 19
25	24	rspcva 3134	. . . . . . . . . . . . . . . . . 18 $/\$
26	25	2a1d 26	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
27	26	expcom 442	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
28	27	com24 89	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
29	28	imp31 439	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
30	7, 29	syl5bi 225	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
31	30	con4d 108	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
32	31	ralrimiva 2809	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
33	32	ex 441	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	34	com12 31	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
36	35	reximdva 2858	. . . . . . 7 $/\$ $/\$ $/\$
37		ssrexv 3480	. . . . . . 7
38	22, 36, 37	sylsyld 57	. . . . . 6 $/\$ $/\$ $/\$
39	21, 38	mpd 15	. . . . 5 $/\$ $/\$
40	39	3exp 1230	. . . 4
41	40	com3l 83	. . 3
42	14, 41	pm2.61ine 2726	. 2
43		fzfi 12223	. . . . 5
44		elfz2nn0 11911	. . . . . . . . . . 11 $/\$ $/\$
45	44	notbii 303	. . . . . . . . . 10 $/\$ $/\$
46		3ianor 1024	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$
47		3orass 1010	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
48	45, 46, 47	3bitri 279	. . . . . . . . 9 $\/$ $\/$
49		ssel 3412	. . . . . . . . . . . . 13
50	49	adantr 472	. . . . . . . . . . . 12 $/\$
51	50	adantr 472	. . . . . . . . . . 11 $/\$ $/\$
52	51	con3rr3 143	. . . . . . . . . 10 $/\$ $/\$
53		notnot 297	. . . . . . . . . . . 12
54		pm2.24 112	. . . . . . . . . . . . . . . . 17
55	54	adantl 473	. . . . . . . . . . . . . . . 16 $/\$
56	55	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	com12 31	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	a1d 25	. . . . . . . . . . . . 13 $/\$ $/\$
59		breq2 4399	. . . . . . . . . . . . . . . . . . . 20
60		neleq1 2748	. . . . . . . . . . . . . . . . . . . 20
61	59, 60	imbi12d 327	. . . . . . . . . . . . . . . . . . 19
62	61	rspcva 3134	. . . . . . . . . . . . . . . . . 18 $/\$
63		nn0re 10902	. . . . . . . . . . . . . . . . . . . . . . . . 25
64		nn0re 10902	. . . . . . . . . . . . . . . . . . . . . . . . 25
65		ltnle 9731	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
66	63, 64, 65	syl2an 485	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
67		df-nel 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
69	66, 68	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
70	69	biimpd 212	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
71	70	ex 441	. . . . . . . . . . . . . . . . . . . . 21
72	71	adantl 473	. . . . . . . . . . . . . . . . . . . 20 $/\$
73	72	com12 31	. . . . . . . . . . . . . . . . . . 19 $/\$
74	73	adantr 472	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
75	62, 74	mpid 41	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
76	75	ex 441	. . . . . . . . . . . . . . . 16 $/\$
77	76	com13 82	. . . . . . . . . . . . . . 15 $/\$
78	77	imp 436	. . . . . . . . . . . . . 14 $/\$ $/\$
79	78	com13 82	. . . . . . . . . . . . 13 $/\$ $/\$
80	58, 79	jaoi 386	. . . . . . . . . . . 12 $\/$ $/\$ $/\$
81	53, 80	syl5bir 226	. . . . . . . . . . 11 $\/$ $/\$ $/\$
82	81	impcom 437	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
83	52, 82	jaoi3 980	. . . . . . . . 9 $\/$ $\/$ $/\$ $/\$
84	48, 83	sylbi 200	. . . . . . . 8 $/\$ $/\$
85	84	com12 31	. . . . . . 7 $/\$ $/\$
86	85	con4d 108	. . . . . 6 $/\$ $/\$
87	86	ssrdv 3424	. . . . 5 $/\$ $/\$
88		ssfi 7810	. . . . 5 $/\$
89	43, 87, 88	sylancr 676	. . . 4 $/\$ $/\$
90	89	ex 441	. . 3 $/\$
91	90	rexlimdva 2871	. 2
92	42, 91	impbid 195	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wnel 2642

wral 2756

wrex 2757

wss 3390

c0 3722 class class class wbr 4395

wor 4759 (class class class)co 6308

cfn 7587

cr 9556

cc0 9557

clt 9693

cle 9694

cn0 10893

cfz 11810

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811

This theorem is referenced by: rabssnn0fi 12236

W3C validator