nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4763

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4677 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6762 or nntri3or 6756), 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 3333	. . . 4 $\/$ $/\$
2		peano1 4736	. . . . 5
3		suc0 4551	. . . . . 6
4		peano2 4737	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2312	. . . . 5
7		prssi 3868	. . . . 5 $/\$
8	2, 6, 7	mp2an 430	. . . 4
9	1, 8	sstri 3257	. . 3 $\/$ $/\$
10		eqid 2238	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4674	. . 3 $\/$ $/\$
12		pp0ex 4321	. . . . 5
13	12	rabex 4275	. . . 4 $\/$ $/\$
14		sseq1 3271	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2302	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1878	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 477	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2302	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 677	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1877	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 477	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1878	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2877	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 430	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4675	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wal 1400

wceq 1402

wex 1545

wcel 2209

crab 2532

wss 3220

c0 3520

csn 3705

cpr 3706

csuc 4505

com 4732

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 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4244 ax-nul 4254 ax-pow 4306 ax-pr 4341 ax-un 4573

This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-rab 2537 df-v 2823 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-pw 3687 df-sn 3711 df-pr 3712 df-uni 3931 df-int 3966 df-suc 4511 df-iom 4733

This theorem is referenced by: (None)

W3C validator