nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4669

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4583 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6585 or nntri3or 6579), 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 3278	. . . 4 $\/$ $/\$
2		peano1 4642	. . . . 5
3		suc0 4458	. . . . . 6
4		peano2 4643	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2279	. . . . 5
7		prssi 3791	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3202	. . 3 $\/$ $/\$
10		eqid 2205	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4580	. . 3 $\/$ $/\$
12		pp0ex 4233	. . . . 5
13	12	rabex 4188	. . . 4 $\/$ $/\$
14		sseq1 3216	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2269	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1848	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2269	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 669	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1847	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1848	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2827	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4581	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wal 1371

wceq 1373

wex 1515

wcel 2176

crab 2488

wss 3166

c0 3460

csn 3633

cpr 3634

csuc 4412

com 4638

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 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-nul 4170 ax-pow 4218 ax-pr 4253 ax-un 4480

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-rab 2493 df-v 2774 df-dif 3168 df-un 3170 df-in 3172 df-ss 3179 df-nul 3461 df-pw 3618 df-sn 3639 df-pr 3640 df-uni 3851 df-int 3886 df-suc 4418 df-iom 4639

This theorem is referenced by: (None)

W3C validator