nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4712

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4626 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6643 or nntri3or 6637), 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 3309	. . . 4 $\/$ $/\$
2		peano1 4685	. . . . 5
3		suc0 4501	. . . . . 6
4		peano2 4686	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2303	. . . . 5
7		prssi 3825	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3233	. . 3 $\/$ $/\$
10		eqid 2229	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4623	. . 3 $\/$ $/\$
12		pp0ex 4272	. . . . 5
13	12	rabex 4227	. . . 4 $\/$ $/\$
14		sseq1 3247	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2293	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1871	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2293	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 671	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1870	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1871	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2855	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4624	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wal 1393

wceq 1395

wex 1538

wcel 2200

crab 2512

wss 3197

c0 3491

csn 3666

cpr 3667

csuc 4455

com 4681

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-rab 2517 df-v 2801 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-uni 3888 df-int 3923 df-suc 4461 df-iom 4682

This theorem is referenced by: (None)

W3C validator