frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6565

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 4944	. . . . . . . . . 10
2	1	biantrur 303	. . . . . . . . 9 $/\$
3		vex 2804	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4514	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2447	. . . . . . . . . . . . . 14
7	1	eqeq1i 2238	. . . . . . . . . . . . . 14
8	6, 7	mtbir 677	. . . . . . . . . . . . 13
9	8	intnanr 937	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2623	. . . . . . . . . 10 $/\$
12	11	biorfi 753	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 735	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 206	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2346	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2351	. . . . . . 7
17	15, 16	eqtr3i 2253	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2813	. . . . . 6
19	17, 18	eqeltrid 2317	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4215	. . . . . . 7
21		dmeq 4930	. . . . . . . . . . . . 13
22	21	eqeq1d 2239	. . . . . . . . . . . 12
23		fveq1 5638	. . . . . . . . . . . . . 14
24	23	fveq2d 5643	. . . . . . . . . . . . 13
25	24	eleq2d 2300	. . . . . . . . . . . 12
26	22, 25	anbi12d 473	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2532	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2239	. . . . . . . . . . 11
29	28	anbi1d 465	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 800	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2348	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2230	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5722	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 424	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2279	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2307	. . 3 $/\$ $\/$ $/\$
38		df-frec 6559	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5640	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4691	. . . . . 6
41		fvres 5663	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2251	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2230	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6491	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2275	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2263	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1397

wcel 2201

cab 2216

wne 2401

wrex 2510

cvv 2801

c0 3493

cmpt 4149

csuc 4461

com 4687

cdm 4724

cres 4726

cfv 5325 recscrecs 6472 freccfrec 6558

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 2203 ax-14 2204 ax-ext 2212 ax-sep 4206 ax-nul 4214 ax-pow 4263 ax-pr 4298 ax-un 4529 ax-setind 4634

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1810 df-eu 2081 df-mo 2082 df-clab 2217 df-cleq 2223 df-clel 2226 df-nfc 2362 df-ne 2402 df-ral 2514 df-rex 2515 df-rab 2518 df-v 2803 df-sbc 3031 df-csb 3127 df-dif 3201 df-un 3203 df-in 3205 df-ss 3212 df-nul 3494 df-pw 3653 df-sn 3674 df-pr 3675 df-op 3677 df-uni 3893 df-int 3928 df-iun 3971 df-br 4088 df-opab 4150 df-mpt 4151 df-tr 4187 df-id 4389 df-iord 4462 df-on 4464 df-suc 4467 df-iom 4688 df-xp 4730 df-rel 4731 df-cnv 4732 df-co 4733 df-dm 4734 df-res 4736 df-iota 5285 df-fun 5327 df-fn 5328 df-fv 5333 df-recs 6473 df-frec 6559

This theorem is referenced by: frecrdg 6576 frec2uz0d 10664 frec2uzrdg 10674 frecuzrdg0 10678 frecuzrdgg 10681 frecuzrdg0t 10687 seq3val 10725 seqvalcd 10726

W3C validator