frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6562

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 4945	. . . . . . . . . 10
2	1	biantrur 303	. . . . . . . . 9 $/\$
3		vex 2805	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4515	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2448	. . . . . . . . . . . . . 14
7	1	eqeq1i 2239	. . . . . . . . . . . . . 14
8	6, 7	mtbir 677	. . . . . . . . . . . . 13
9	8	intnanr 937	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2624	. . . . . . . . . 10 $/\$
12	11	biorfi 753	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 735	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 206	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2347	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2352	. . . . . . 7
17	15, 16	eqtr3i 2254	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2814	. . . . . 6
19	17, 18	eqeltrid 2318	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4216	. . . . . . 7
21		dmeq 4931	. . . . . . . . . . . . 13
22	21	eqeq1d 2240	. . . . . . . . . . . 12
23		fveq1 5638	. . . . . . . . . . . . . 14
24	23	fveq2d 5643	. . . . . . . . . . . . 13
25	24	eleq2d 2301	. . . . . . . . . . . 12
26	22, 25	anbi12d 473	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2533	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2240	. . . . . . . . . . 11
29	28	anbi1d 465	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 800	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2349	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2231	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5722	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 424	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2280	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2308	. . 3 $/\$ $\/$ $/\$
38		df-frec 6556	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5640	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4692	. . . . . 6
41		fvres 5663	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2252	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2231	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6488	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2276	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2264	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1397

wcel 2202

cab 2217

wne 2402

wrex 2511

cvv 2802

c0 3494

cmpt 4150

csuc 4462

com 4688

cdm 4725

cres 4727

cfv 5326 recscrecs 6469 freccfrec 6555

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 ax-setind 4635

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-fal 1403 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ne 2403 df-ral 2515 df-rex 2516 df-rab 2519 df-v 2804 df-sbc 3032 df-csb 3128 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-op 3678 df-uni 3894 df-int 3929 df-iun 3972 df-br 4089 df-opab 4151 df-mpt 4152 df-tr 4188 df-id 4390 df-iord 4463 df-on 4465 df-suc 4468 df-iom 4689 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-res 4737 df-iota 5286 df-fun 5328 df-fn 5329 df-fv 5334 df-recs 6470 df-frec 6556

This theorem is referenced by: frecrdg 6573 frec2uz0d 10660 frec2uzrdg 10670 frecuzrdg0 10674 frecuzrdgg 10677 frecuzrdg0t 10683 seq3val 10721 seqvalcd 10722

W3C validator