frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6628

Description: The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)

**Assertion**
Ref	Expression
frec0g	frec

Proof of Theorem frec0g Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dm0 4970	. . . . . . . . . 10
2	1	biantrur 303	. . . . . . . . 9 $/\$
3		vex 2816	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4539	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2458	. . . . . . . . . . . . . 14
7	1	eqeq1i 2240	. . . . . . . . . . . . . 14
8	6, 7	mtbir 678	. . . . . . . . . . . . 13
9	8	intnanr 938	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2634	. . . . . . . . . 10 $/\$
12	11	biorfi 754	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 736	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 206	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2348	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2355	. . . . . . 7
17	15, 16	eqtr3i 2255	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2825	. . . . . 6
19	17, 18	eqeltrid 2319	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4237	. . . . . . 7
21		dmeq 4956	. . . . . . . . . . . . 13
22	21	eqeq1d 2241	. . . . . . . . . . . 12
23		fveq1 5669	. . . . . . . . . . . . . 14
24	23	fveq2d 5674	. . . . . . . . . . . . 13
25	24	eleq2d 2302	. . . . . . . . . . . 12
26	22, 25	anbi12d 473	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2543	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2241	. . . . . . . . . . 11
29	28	anbi1d 465	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 801	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2352	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2232	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5753	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 424	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2281	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2309	. . 3 $/\$ $\/$ $/\$
38		df-frec 6622	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5671	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4716	. . . . . 6
41		fvres 5694	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2253	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2232	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6554	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2277	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2265	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1398

wcel 2203

cab 2218

wne 2412

wrex 2521

cvv 2813

c0 3508

cmpt 4171

csuc 4486

com 4712

cdm 4749

cres 4751

cfv 5352 recscrecs 6535 freccfrec 6621

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2205 ax-14 2206 ax-ext 2214 ax-sep 4228 ax-nul 4236 ax-pow 4287 ax-pr 4322 ax-un 4554 ax-setind 4659

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-fal 1404 df-nf 1510 df-sb 1812 df-eu 2083 df-mo 2084 df-clab 2219 df-cleq 2225 df-clel 2228 df-nfc 2373 df-ne 2413 df-ral 2525 df-rex 2526 df-rab 2529 df-v 2815 df-sbc 3043 df-csb 3139 df-dif 3213 df-un 3215 df-in 3217 df-ss 3224 df-nul 3509 df-pw 3671 df-sn 3695 df-pr 3696 df-op 3698 df-uni 3915 df-int 3950 df-iun 3993 df-br 4110 df-opab 4172 df-mpt 4173 df-tr 4209 df-id 4414 df-iord 4487 df-on 4489 df-suc 4492 df-iom 4713 df-xp 4755 df-rel 4756 df-cnv 4757 df-co 4758 df-dm 4759 df-res 4761 df-iota 5312 df-fun 5354 df-fn 5355 df-fv 5360 df-recs 6536 df-frec 6622

This theorem is referenced by: frecrdg 6639 frec2uz0d 10761 frec2uzrdg 10771 frecuzrdg0 10775 frecuzrdgg 10778 frecuzrdg0t 10784 seq3val 10822 seqvalcd 10823

W3C validator