frec0g - Intuitionistic Logic Explorer

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

Theorem frec0g 6506

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 4911	. . . . . . . . . 10
2	1	biantrur 303	. . . . . . . . 9 $/\$
3		vex 2779	. . . . . . . . . . . . . . . 16
4		nsuceq0g 4483	. . . . . . . . . . . . . . . 16
5	3, 4	ax-mp 5	. . . . . . . . . . . . . . 15
6	5	nesymi 2424	. . . . . . . . . . . . . 14
7	1	eqeq1i 2215	. . . . . . . . . . . . . 14
8	6, 7	mtbir 673	. . . . . . . . . . . . 13
9	8	intnanr 932	. . . . . . . . . . . 12 $/\$
10	9	a1i 9	. . . . . . . . . . 11 $/\$
11	10	nrex 2600	. . . . . . . . . 10 $/\$
12	11	biorfi 748	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$
13		orcom 730	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
14	2, 12, 13	3bitri 206	. . . . . . . 8 $/\$ $\/$ $/\$
15	14	abbii 2323	. . . . . . 7 $/\$ $\/$ $/\$
16		abid2 2328	. . . . . . 7
17	15, 16	eqtr3i 2230	. . . . . 6 $/\$ $\/$ $/\$
18		elex 2788	. . . . . 6
19	17, 18	eqeltrid 2294	. . . . 5 $/\$ $\/$ $/\$
20		0ex 4187	. . . . . . 7
21		dmeq 4897	. . . . . . . . . . . . 13
22	21	eqeq1d 2216	. . . . . . . . . . . 12
23		fveq1 5598	. . . . . . . . . . . . . 14
24	23	fveq2d 5603	. . . . . . . . . . . . 13
25	24	eleq2d 2277	. . . . . . . . . . . 12
26	22, 25	anbi12d 473	. . . . . . . . . . 11 $/\$ $/\$
27	26	rexbidv 2509	. . . . . . . . . 10 $/\$ $/\$
28	21	eqeq1d 2216	. . . . . . . . . . 11
29	28	anbi1d 465	. . . . . . . . . 10 $/\$ $/\$
30	27, 29	orbi12d 795	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
31	30	abbidv 2325	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
32		eqid 2207	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
33	31, 32	fvmptg 5678	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	20, 33	mpan 424	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
35	34, 17	eqtrdi 2256	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
36	19, 35	syl 14	. . . 4 $/\$ $\/$ $/\$
37	36, 18	eqeltrd 2284	. . 3 $/\$ $\/$ $/\$
38		df-frec 6500	. . . . . 6 frec recs $/\$ $\/$ $/\$
39	38	fveq1i 5600	. . . . 5 frec recs $/\$ $\/$ $/\$
40		peano1 4660	. . . . . 6
41		fvres 5623	. . . . . 6 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
42	40, 41	ax-mp 5	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
43	39, 42	eqtri 2228	. . . 4 frec recs $/\$ $\/$ $/\$
44		eqid 2207	. . . . 5 recs $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$
45	44	tfr0 6432	. . . 4 $/\$ $\/$ $/\$ recs $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
46	43, 45	eqtrid 2252	. . 3 $/\$ $\/$ $/\$ frec $/\$ $\/$ $/\$
47	37, 46	syl 14	. 2 frec $/\$ $\/$ $/\$
48	47, 36	eqtrd 2240	1 frec

Colors of variables: wff set class

Syntax hints:

wn 3

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

wceq 1373

wcel 2178

cab 2193

wne 2378

wrex 2487

cvv 2776

c0 3468

cmpt 4121

csuc 4430

com 4656

cdm 4693

cres 4695

cfv 5290 recscrecs 6413 freccfrec 6499

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 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2180 ax-14 2181 ax-ext 2189 ax-sep 4178 ax-nul 4186 ax-pow 4234 ax-pr 4269 ax-un 4498 ax-setind 4603

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2194 df-cleq 2200 df-clel 2203 df-nfc 2339 df-ne 2379 df-ral 2491 df-rex 2492 df-rab 2495 df-v 2778 df-sbc 3006 df-csb 3102 df-dif 3176 df-un 3178 df-in 3180 df-ss 3187 df-nul 3469 df-pw 3628 df-sn 3649 df-pr 3650 df-op 3652 df-uni 3865 df-int 3900 df-iun 3943 df-br 4060 df-opab 4122 df-mpt 4123 df-tr 4159 df-id 4358 df-iord 4431 df-on 4433 df-suc 4436 df-iom 4657 df-xp 4699 df-rel 4700 df-cnv 4701 df-co 4702 df-dm 4703 df-res 4705 df-iota 5251 df-fun 5292 df-fn 5293 df-fv 5298 df-recs 6414 df-frec 6500

This theorem is referenced by: frecrdg 6517 frec2uz0d 10581 frec2uzrdg 10591 frecuzrdg0 10595 frecuzrdgg 10598 frecuzrdg0t 10604 seq3val 10642 seqvalcd 10643

W3C validator