nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4657

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4571 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6557 or nntri3or 6551), 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 3268	. . . 4 $\/$ $/\$
2		peano1 4630	. . . . 5
3		suc0 4446	. . . . . 6
4		peano2 4631	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2270	. . . . 5
7		prssi 3780	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3192	. . 3 $\/$ $/\$
10		eqid 2196	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4568	. . 3 $\/$ $/\$
12		pp0ex 4222	. . . . 5
13	12	rabex 4177	. . . 4 $\/$ $/\$
14		sseq1 3206	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2260	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1839	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2260	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 668	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1838	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1839	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2818	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4569	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wal 1362

wceq 1364

wex 1506

wcel 2167

crab 2479

wss 3157

c0 3450

csn 3622

cpr 3623

csuc 4400

com 4626

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1475 df-sb 1777 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 df-rex 2481 df-rab 2484 df-v 2765 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-pw 3607 df-sn 3628 df-pr 3629 df-uni 3840 df-int 3875 df-suc 4406 df-iom 4627

This theorem is referenced by: (None)

W3C validator