nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4768

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4682 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6772 or nntri3or 6766), 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 4741	. . . . 5
3		suc0 4556	. . . . . 6
4		peano2 4742	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2312	. . . . 5
7		prssi 3873	. . . . 5 $/\$
8	2, 6, 7	mp2an 430	. . . 4
9	1, 8	sstri 3257	. . 3 $\/$ $/\$
10		eqid 2238	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4679	. . 3 $\/$ $/\$
12		pp0ex 4326	. . . . 5
13	12	rabex 4280	. . . 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 4680	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

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

wal 1400

wceq 1402

wex 1545

wcel 2209

crab 2532

wss 3220

c0 3520

csn 3709

cpr 3710

csuc 4510

com 4737

This proof depends on 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 4249 ax-nul 4259 ax-pow 4311 ax-pr 4346 ax-un 4578

This proof 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 3690 df-sn 3715 df-pr 3716 df-uni 3936 df-int 3971 df-suc 4516 df-iom 4738

This theorem is used by: (None)

W3C validator