frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6450

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 4876	. . . . . . . . . 10
2	1	biantrur 303	. . . . . . . . 9 $/\$
3		vex 2763	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4449	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2410	. . . . . . . . . . . . . 14
7	1	eqeq1i 2201	. . . . . . . . . . . . . 14
8	6, 7	mtbir 672	. . . . . . . . . . . . 13
9	8	intnanr 931	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2586	. . . . . . . . . 10 $/\$
12	11	biorfi 747	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 729	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 206	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2309	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2314	. . . . . . 7
17	15, 16	eqtr3i 2216	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2771	. . . . . 6
19	17, 18	eqeltrid 2280	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4156	. . . . . . 7
21		dmeq 4862	. . . . . . . . . . . . 13
22	21	eqeq1d 2202	. . . . . . . . . . . 12
23		fveq1 5553	. . . . . . . . . . . . . 14
24	23	fveq2d 5558	. . . . . . . . . . . . 13
25	24	eleq2d 2263	. . . . . . . . . . . 12
26	22, 25	anbi12d 473	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2495	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2202	. . . . . . . . . . 11
29	28	anbi1d 465	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 794	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2311	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2193	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5633	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 424	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2242	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2270	. . 3 $/\$ $\/$ $/\$
38		df-frec 6444	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5555	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4626	. . . . . 6
41		fvres 5578	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2214	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2193	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6376	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2238	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2226	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1364

wcel 2164

cab 2179

wne 2364

wrex 2473

cvv 2760

c0 3446

cmpt 4090

csuc 4396

com 4622

cdm 4659

cres 4661

cfv 5254 recscrecs 6357 freccfrec 6443

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 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-nul 4155 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-sbc 2986 df-csb 3081 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3447 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-int 3871 df-iun 3914 df-br 4030 df-opab 4091 df-mpt 4092 df-tr 4128 df-id 4324 df-iord 4397 df-on 4399 df-suc 4402 df-iom 4623 df-xp 4665 df-rel 4666 df-cnv 4667 df-co 4668 df-dm 4669 df-res 4671 df-iota 5215 df-fun 5256 df-fn 5257 df-fv 5262 df-recs 6358 df-frec 6444

This theorem is referenced by: frecrdg 6461 frec2uz0d 10470 frec2uzrdg 10480 frecuzrdg0 10484 frecuzrdgg 10487 frecuzrdg0t 10493 seq3val 10531 seqvalcd 10532

W3C validator