frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6365

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 4818	. . . . . . . . . 10
2	1	biantrur 301	. . . . . . . . 9 $/\$
3		vex 2729	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4396	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2382	. . . . . . . . . . . . . 14
7	1	eqeq1i 2173	. . . . . . . . . . . . . 14
8	6, 7	mtbir 661	. . . . . . . . . . . . 13
9	8	intnanr 920	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2558	. . . . . . . . . 10 $/\$
12	11	biorfi 736	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 718	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 205	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2282	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2287	. . . . . . 7
17	15, 16	eqtr3i 2188	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2737	. . . . . 6
19	17, 18	eqeltrid 2253	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4109	. . . . . . 7
21		dmeq 4804	. . . . . . . . . . . . 13
22	21	eqeq1d 2174	. . . . . . . . . . . 12
23		fveq1 5485	. . . . . . . . . . . . . 14
24	23	fveq2d 5490	. . . . . . . . . . . . 13
25	24	eleq2d 2236	. . . . . . . . . . . 12
26	22, 25	anbi12d 465	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2467	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2174	. . . . . . . . . . 11
29	28	anbi1d 461	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 783	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2284	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2165	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5562	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 421	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2215	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2243	. . 3 $/\$ $\/$ $/\$
38		df-frec 6359	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5487	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4571	. . . . . 6
41		fvres 5510	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2186	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2165	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6291	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	syl5eq 2211	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2198	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1343

wcel 2136

cab 2151

wne 2336

wrex 2445

cvv 2726

c0 3409

cmpt 4043

csuc 4343

com 4567

cdm 4604

cres 4606

cfv 5188 recscrecs 6272 freccfrec 6358

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1435 ax-7 1436 ax-gen 1437 ax-ie1 1481 ax-ie2 1482 ax-8 1492 ax-10 1493 ax-11 1494 ax-i12 1495 ax-bndl 1497 ax-4 1498 ax-17 1514 ax-i9 1518 ax-ial 1522 ax-i5r 1523 ax-13 2138 ax-14 2139 ax-ext 2147 ax-sep 4100 ax-nul 4108 ax-pow 4153 ax-pr 4187 ax-un 4411 ax-setind 4514

This theorem depends on definitions: df-bi 116 df-3an 970 df-tru 1346 df-fal 1349 df-nf 1449 df-sb 1751 df-eu 2017 df-mo 2018 df-clab 2152 df-cleq 2158 df-clel 2161 df-nfc 2297 df-ne 2337 df-ral 2449 df-rex 2450 df-rab 2453 df-v 2728 df-sbc 2952 df-csb 3046 df-dif 3118 df-un 3120 df-in 3122 df-ss 3129 df-nul 3410 df-pw 3561 df-sn 3582 df-pr 3583 df-op 3585 df-uni 3790 df-int 3825 df-iun 3868 df-br 3983 df-opab 4044 df-mpt 4045 df-tr 4081 df-id 4271 df-iord 4344 df-on 4346 df-suc 4349 df-iom 4568 df-xp 4610 df-rel 4611 df-cnv 4612 df-co 4613 df-dm 4614 df-res 4616 df-iota 5153 df-fun 5190 df-fn 5191 df-fv 5196 df-recs 6273 df-frec 6359

This theorem is referenced by: frecrdg 6376 frec2uz0d 10334 frec2uzrdg 10344 frecuzrdg0 10348 frecuzrdgg 10351 frecuzrdg0t 10357 seq3val 10393 seqvalcd 10394

W3C validator