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 12204

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 10891	. . . . . 6
2	1	a1i 11	. . . . 5
3		breq1 4408	. . . . . . . 8
4	3	imbi1d 319	. . . . . . 7
5	4	ralbidv 2829	. . . . . 6
6	5	adantl 468	. . . . 5 $/\$
7		nnel 2735	. . . . . . . . 9
8		n0i 3738	. . . . . . . . 9
9	7, 8	sylbi 199	. . . . . . . 8
10	9	con4i 134	. . . . . . 7
11	10	a1d 26	. . . . . 6
12	11	ralrimivw 2805	. . . . 5
13	2, 6, 12	rspcedvd 3157	. . . 4
14	13	2a1d 27	. . 3
15		ltso 9719	. . . . . . 7
16		id 22	. . . . . . . . 9
17		nn0ssre 10880	. . . . . . . . 9
18	16, 17	syl6ss 3446	. . . . . . . 8
19	18	3anim3i 1197	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
20		fisup2g 7989	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
21	15, 19, 20	sylancr 670	. . . . . 6 $/\$ $/\$ $/\$
22		simp3 1011	. . . . . . 7 $/\$ $/\$
23		breq2 4409	. . . . . . . . . . . . . . . . . . . 20
24	23	notbid 296	. . . . . . . . . . . . . . . . . . 19
25	24	rspcva 3150	. . . . . . . . . . . . . . . . . 18 $/\$
26	25	2a1d 27	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$
27	26	expcom 437	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
28	27	com24 90	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
29	28	imp31 434	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
30	7, 29	syl5bi 221	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
31	30	con4d 109	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
32	31	ralrimiva 2804	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
33	32	ex 436	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	33	adantr 467	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
35	34	com12 32	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
36	35	reximdva 2864	. . . . . . 7 $/\$ $/\$ $/\$
37		ssrexv 3496	. . . . . . 7
38	22, 36, 37	sylsyld 58	. . . . . 6 $/\$ $/\$ $/\$
39	21, 38	mpd 15	. . . . 5 $/\$ $/\$
40	39	3exp 1208	. . . 4
41	40	com3l 84	. . 3
42	14, 41	pm2.61ine 2709	. 2
43		fzfi 12192	. . . . 5
44		elfz2nn0 11892	. . . . . . . . . . 11 $/\$ $/\$
45	44	notbii 298	. . . . . . . . . 10 $/\$ $/\$
46		3ianor 1003	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$
47		3orass 989	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
48	45, 46, 47	3bitri 275	. . . . . . . . 9 $\/$ $\/$
49		ssel 3428	. . . . . . . . . . . . 13
50	49	adantr 467	. . . . . . . . . . . 12 $/\$
51	50	adantr 467	. . . . . . . . . . 11 $/\$ $/\$
52	51	con3rr3 142	. . . . . . . . . 10 $/\$ $/\$
53		notnot 293	. . . . . . . . . . . 12
54		pm2.24 113	. . . . . . . . . . . . . . . . 17
55	54	adantl 468	. . . . . . . . . . . . . . . 16 $/\$
56	55	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $/\$
57	56	com12 32	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	a1d 26	. . . . . . . . . . . . 13 $/\$ $/\$
59		breq2 4409	. . . . . . . . . . . . . . . . . . . 20
60		neleq1 2731	. . . . . . . . . . . . . . . . . . . 20
61	59, 60	imbi12d 322	. . . . . . . . . . . . . . . . . . 19
62	61	rspcva 3150	. . . . . . . . . . . . . . . . . 18 $/\$
63		nn0re 10885	. . . . . . . . . . . . . . . . . . . . . . . . 25
64		nn0re 10885	. . . . . . . . . . . . . . . . . . . . . . . . 25
65		ltnle 9718	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
66	63, 64, 65	syl2an 480	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
67		df-nel 2627	. . . . . . . . . . . . . . . . . . . . . . . . 25
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
69	66, 68	imbi12d 322	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
70	69	biimpd 211	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
71	70	ex 436	. . . . . . . . . . . . . . . . . . . . 21
72	71	adantl 468	. . . . . . . . . . . . . . . . . . . 20 $/\$
73	72	com12 32	. . . . . . . . . . . . . . . . . . 19 $/\$
74	73	adantr 467	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
75	62, 74	mpid 42	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
76	75	ex 436	. . . . . . . . . . . . . . . 16 $/\$
77	76	com13 83	. . . . . . . . . . . . . . 15 $/\$
78	77	imp 431	. . . . . . . . . . . . . 14 $/\$ $/\$
79	78	com13 83	. . . . . . . . . . . . 13 $/\$ $/\$
80	58, 79	jaoi 381	. . . . . . . . . . . 12 $\/$ $/\$ $/\$
81	53, 80	syl5bir 222	. . . . . . . . . . 11 $\/$ $/\$ $/\$
82	81	impcom 432	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$
83	52, 82	jaoi3 982	. . . . . . . . 9 $\/$ $\/$ $/\$ $/\$
84	48, 83	sylbi 199	. . . . . . . 8 $/\$ $/\$
85	84	com12 32	. . . . . . 7 $/\$ $/\$
86	85	con4d 109	. . . . . 6 $/\$ $/\$
87	86	ssrdv 3440	. . . . 5 $/\$ $/\$
88		ssfi 7797	. . . . 5 $/\$
89	43, 87, 88	sylancr 670	. . . 4 $/\$ $/\$
90	89	ex 436	. . 3 $/\$
91	90	rexlimdva 2881	. 2
92	42, 91	impbid 194	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $\/$ w3o 985 $/\$ w3a 986

wceq 1446

wcel 1889

wne 2624

wnel 2625

wral 2739

wrex 2740

wss 3406

c0 3733 class class class wbr 4405

wor 4757 (class class class)co 6295

cfn 7574

cr 9543

cc0 9544

clt 9680

cle 9681

cn0 10876

cfz 11791

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pow 4584 ax-pr 4642 ax-un 6588 ax-cnex 9600 ax-resscn 9601 ax-1cn 9602 ax-icn 9603 ax-addcl 9604 ax-addrcl 9605 ax-mulcl 9606 ax-mulrcl 9607 ax-mulcom 9608 ax-addass 9609 ax-mulass 9610 ax-distr 9611 ax-i2m1 9612 ax-1ne0 9613 ax-1rid 9614 ax-rnegex 9615 ax-rrecex 9616 ax-cnre 9617 ax-pre-lttri 9618 ax-pre-lttrn 9619 ax-pre-ltadd 9620 ax-pre-mulgt0 9621

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-nel 2627 df-ral 2744 df-rex 2745 df-reu 2746 df-rmo 2747 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-iun 4283 df-br 4406 df-opab 4465 df-mpt 4466 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-pred 5383 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fn 5588 df-f 5589 df-f1 5590 df-fo 5591 df-f1o 5592 df-fv 5593 df-riota 6257 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-er 7368 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-pnf 9682 df-mnf 9683 df-xr 9684 df-ltxr 9685 df-le 9686 df-sub 9867 df-neg 9868 df-nn 10617 df-n0 10877 df-z 10945 df-uz 11167 df-fz 11792

This theorem is referenced by: rabssnn0fi 12205

W3C validator