nnregexmid - Intuitionistic Logic Explorer

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

Theorem nnregexmid 4719

Description: If inhabited sets of natural numbers always have minimal elements, excluded middle follows. The argument is essentially the same as regexmid 4633 and the larger lesson is that although natural numbers may behave "non-constructively" even in a constructive set theory (for example see nndceq 6666 or nntri3or 6660), 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 3312	. . . 4 $\/$ $/\$
2		peano1 4692	. . . . 5
3		suc0 4508	. . . . . 6
4		peano2 4693	. . . . . . 7
5	2, 4	ax-mp 5	. . . . . 6
6	3, 5	eqeltrri 2305	. . . . 5
7		prssi 3831	. . . . 5 $/\$
8	2, 6, 7	mp2an 426	. . . 4
9	1, 8	sstri 3236	. . 3 $\/$ $/\$
10		eqid 2231	. . . 4 $\/$ $/\$ $\/$ $/\$
11	10	regexmidlemm 4630	. . 3 $\/$ $/\$
12		pp0ex 4279	. . . . 5
13	12	rabex 4234	. . . 4 $\/$ $/\$
14		sseq1 3250	. . . . . 6 $\/$ $/\$ $\/$ $/\$
15		eleq2 2295	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
16	15	exbidv 1873	. . . . . 6 $\/$ $/\$ $\/$ $/\$
17	14, 16	anbi12d 473	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
18		eleq2 2295	. . . . . . . . . 10 $\/$ $/\$ $\/$ $/\$
19	18	notbid 673	. . . . . . . . 9 $\/$ $/\$ $\/$ $/\$
20	19	imbi2d 230	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$
21	20	albidv 1872	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
22	15, 21	anbi12d 473	. . . . . 6 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
23	22	exbidv 1873	. . . . 5 $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
24	17, 23	imbi12d 234	. . . 4 $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
25		nnregexmid.1	. . . 4 $/\$ $/\$
26	13, 24, 25	vtocl 2858	. . 3 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
27	9, 11, 26	mp2an 426	. 2 $\/$ $/\$ $/\$ $\/$ $/\$
28	10	regexmidlem1 4631	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$
29	27, 28	ax-mp 5	1 $\/$

Colors of variables: wff set class

Syntax hints:

wn 3

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

wal 1395

wceq 1397

wex 1540

wcel 2202

crab 2514

wss 3200

c0 3494

csn 3669

cpr 3670

csuc 4462

com 4688

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 619 ax-in2 620 ax-io 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-nul 4215 ax-pow 4264 ax-pr 4299 ax-un 4530

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-dif 3202 df-un 3204 df-in 3206 df-ss 3213 df-nul 3495 df-pw 3654 df-sn 3675 df-pr 3676 df-uni 3894 df-int 3929 df-suc 4468 df-iom 4689

This theorem is referenced by: (None)

W3C validator