nnregexmid - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > nnregexmid		Unicode version

Theorem nnregexmid 4614

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4528 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6490 or nntri3or 6484), sets of natural numbers are a different animal. (Contributed by Jim Kingdon, 6-Sep-2019.)

**Hypothesis**
Ref	Expression
nnregexmid.1	$/\$ $/\$

**Assertion**
Ref	Expression
nnregexmid	$\/$

Distinct variable group:

Proof of Theorem nnregexmid Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssrab2 3238	. . . 4 $\/$ $/\$
2		peano1 4587	. . . . 5
3		suc0 4405	. . . . . 6
4		peano2 4588	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2249	. . . . 5
7		prssi 3747	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3162	. . 3 $\/$ $/\$
10		eqid 2175	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4525	. . 3 $\/$ $/\$
12		pp0ex 4184	. . . . 5
13	12	rabex 4142	. . . 4 $\/$ $/\$
14		sseq1 3176	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2239	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1823	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2239	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 667	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1822	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1823	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2789	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4526	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104 $\/$ wo 708

wal 1351

wceq 1353

wex 1490

wcel 2146

crab 2457

wss 3127

c0 3420

csn 3589

cpr 3590

csuc 4359

com 4583

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-13 2148 ax-14 2149 ax-ext 2157 ax-sep 4116 ax-nul 4124 ax-pow 4169 ax-pr 4203 ax-un 4427

This theorem depends on definitions: df-bi 117 df-3an 980 df-tru 1356 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ral 2458 df-rex 2459 df-rab 2462 df-v 2737 df-dif 3129 df-un 3131 df-in 3133 df-ss 3140 df-nul 3421 df-pw 3574 df-sn 3595 df-pr 3596 df-uni 3806 df-int 3841 df-suc 4365 df-iom 4584

This theorem is referenced by: (None)

W3C validator