nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4687

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4601 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6608 or nntri3or 6602), 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 3286	. . . 4 $\/$ $/\$
2		peano1 4660	. . . . 5
3		suc0 4476	. . . . . 6
4		peano2 4661	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2281	. . . . 5
7		prssi 3802	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3210	. . 3 $\/$ $/\$
10		eqid 2207	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4598	. . 3 $\/$ $/\$
12		pp0ex 4249	. . . . 5
13	12	rabex 4204	. . . 4 $\/$ $/\$
14		sseq1 3224	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2271	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1849	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2271	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 669	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1848	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1849	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2832	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4599	. 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 1516

wcel 2178

crab 2490

wss 3174

c0 3468

csn 3643

cpr 3644

csuc 4430

com 4656

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 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1485 df-sb 1787 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ral 2491 df-rex 2492 df-rab 2495 df-v 2778 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-pw 3628 df-sn 3649 df-pr 3650 df-uni 3865 df-int 3900 df-suc 4436 df-iom 4657

This theorem is referenced by: (None)

W3C validator