frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6380

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 4826	. . . . . . . . . 10
2	1	biantrur 301	. . . . . . . . 9 $/\$
3		vex 2734	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4404	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2387	. . . . . . . . . . . . . 14
7	1	eqeq1i 2179	. . . . . . . . . . . . . 14
8	6, 7	mtbir 667	. . . . . . . . . . . . 13
9	8	intnanr 926	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2563	. . . . . . . . . 10 $/\$
12	11	biorfi 742	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 724	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 205	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2287	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2292	. . . . . . 7
17	15, 16	eqtr3i 2194	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2742	. . . . . 6
19	17, 18	eqeltrid 2258	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4117	. . . . . . 7
21		dmeq 4812	. . . . . . . . . . . . 13
22	21	eqeq1d 2180	. . . . . . . . . . . 12
23		fveq1 5498	. . . . . . . . . . . . . 14
24	23	fveq2d 5503	. . . . . . . . . . . . 13
25	24	eleq2d 2241	. . . . . . . . . . . 12
26	22, 25	anbi12d 471	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2472	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2180	. . . . . . . . . . 11
29	28	anbi1d 463	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 789	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2289	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2171	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5576	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 422	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2220	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2248	. . 3 $/\$ $\/$ $/\$
38		df-frec 6374	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5500	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4579	. . . . . 6
41		fvres 5523	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2192	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2171	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6306	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2216	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2204	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1349

wcel 2142

cab 2157

wne 2341

wrex 2450

cvv 2731

c0 3415

cmpt 4051

csuc 4351

com 4575

cdm 4612

cres 4614

cfv 5200 recscrecs 6287 freccfrec 6373

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 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522

This theorem depends on definitions: df-bi 116 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-ral 2454 df-rex 2455 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-iord 4352 df-on 4354 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-res 4624 df-iota 5162 df-fun 5202 df-fn 5203 df-fv 5208 df-recs 6288 df-frec 6374

This theorem is referenced by: frecrdg 6391 frec2uz0d 10359 frec2uzrdg 10369 frecuzrdg0 10373 frecuzrdgg 10376 frecuzrdg0t 10382 seq3val 10418 seqvalcd 10419

W3C validator