frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6224

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 4691	. . . . . . . . . 10
2	1	biantrur 299	. . . . . . . . 9 $/\$
3		vex 2644	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4278	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 7	. . . . . . . . . . . . . . 15
6	5	nesymi 2313	. . . . . . . . . . . . . 14
7	1	eqeq1i 2107	. . . . . . . . . . . . . 14
8	6, 7	mtbir 637	. . . . . . . . . . . . 13
9	8	intnanr 883	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2483	. . . . . . . . . 10 $/\$
12	11	biorfi 706	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 688	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 205	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2215	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2220	. . . . . . 7
17	15, 16	eqtr3i 2122	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2652	. . . . . 6
19	17, 18	syl5eqel 2186	. . . . 5 $/\$ $\/$ $/\$
20		0ex 3995	. . . . . . 7
21		dmeq 4677	. . . . . . . . . . . . 13
22	21	eqeq1d 2108	. . . . . . . . . . . 12
23		fveq1 5352	. . . . . . . . . . . . . 14
24	23	fveq2d 5357	. . . . . . . . . . . . 13
25	24	eleq2d 2169	. . . . . . . . . . . 12
26	22, 25	anbi12d 460	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2397	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2108	. . . . . . . . . . 11
29	28	anbi1d 456	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 748	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2217	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2100	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5429	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 418	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	syl6eq 2148	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2176	. . 3 $/\$ $\/$ $/\$
38		df-frec 6218	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5354	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4446	. . . . . 6
41		fvres 5377	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 7	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2120	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2100	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6150	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	syl5eq 2144	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2132	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103 $\/$ wo 670

wceq 1299

wcel 1448

cab 2086

wne 2267

wrex 2376

cvv 2641

c0 3310

cmpt 3929

csuc 4225

com 4442

cdm 4477

cres 4479

cfv 5059 recscrecs 6131 freccfrec 6217

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-nul 3994 ax-pow 4038 ax-pr 4069 ax-un 4293 ax-setind 4390

This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-fal 1305 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ne 2268 df-ral 2380 df-rex 2381 df-rab 2384 df-v 2643 df-sbc 2863 df-csb 2956 df-dif 3023 df-un 3025 df-in 3027 df-ss 3034 df-nul 3311 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-int 3719 df-iun 3762 df-br 3876 df-opab 3930 df-mpt 3931 df-tr 3967 df-id 4153 df-iord 4226 df-on 4228 df-suc 4231 df-iom 4443 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-res 4489 df-iota 5024 df-fun 5061 df-fn 5062 df-fv 5067 df-recs 6132 df-frec 6218

This theorem is referenced by: frecrdg 6235 frec2uz0d 10013 frec2uzrdg 10023 frecuzrdg0 10027 frecuzrdgg 10030 frecuzrdg0t 10036 seq3val 10072 seqvalcd 10073

W3C validator