tfr0dm - Intuitionistic Logic Explorer

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

Theorem tfr0dm 6468

Description: Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.)

**Hypothesis**
Ref	Expression
tfr.1	recs

**Assertion**
Ref	Expression
tfr0dm

Proof of Theorem tfr0dm Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4211	. . . . 5
2		opexg 4314	. . . . 5 $/\$
3	1, 2	mpan 424	. . . 4
4		snidg 3695	. . . 4
5	3, 4	syl 14	. . 3
6		fnsng 5368	. . . . 5 $/\$
7	1, 6	mpan 424	. . . 4
8		fvsng 5835	. . . . . . 7 $/\$
9	1, 8	mpan 424	. . . . . 6
10		res0 5009	. . . . . . 7
11	10	fveq2i 5630	. . . . . 6
12	9, 11	eqtr4di 2280	. . . . 5
13		fveq2 5627	. . . . . . 7
14		reseq2 5000	. . . . . . . 8
15	14	fveq2d 5631	. . . . . . 7
16	13, 15	eqeq12d 2244	. . . . . 6
17	1, 16	ralsn 3709	. . . . 5
18	12, 17	sylibr 134	. . . 4
19		suc0 4502	. . . . . 6
20		0elon 4483	. . . . . . 7
21	20	onsuci 4608	. . . . . 6
22	19, 21	eqeltrri 2303	. . . . 5
23		fneq2 5410	. . . . . . 7
24		raleq 2728	. . . . . . 7
25	23, 24	anbi12d 473	. . . . . 6 $/\$ $/\$
26	25	rspcev 2907	. . . . 5 $/\$ $/\$ $/\$
27	22, 26	mpan 424	. . . 4 $/\$ $/\$
28	7, 18, 27	syl2anc 411	. . 3 $/\$
29		snexg 4268	. . . . 5
30		eleq2 2293	. . . . . . 7
31		fneq1 5409	. . . . . . . . 9
32		fveq1 5626	. . . . . . . . . . 11
33		reseq1 4999	. . . . . . . . . . . 12
34	33	fveq2d 5631	. . . . . . . . . . 11
35	32, 34	eqeq12d 2244	. . . . . . . . . 10
36	35	ralbidv 2530	. . . . . . . . 9
37	31, 36	anbi12d 473	. . . . . . . 8 $/\$ $/\$
38	37	rexbidv 2531	. . . . . . 7 $/\$ $/\$
39	30, 38	anbi12d 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$
40	39	spcegv 2891	. . . . 5 $/\$ $/\$ $/\$ $/\$
41	3, 29, 40	3syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$
42		tfr.1	. . . . . 6 recs
43	42	eleq2i 2296	. . . . 5 recs
44		df-recs 6451	. . . . . 6 recs $/\$
45	44	eleq2i 2296	. . . . 5 recs $/\$
46		eluniab 3900	. . . . 5 $/\$ $/\$ $/\$
47	43, 45, 46	3bitri 206	. . . 4 $/\$ $/\$
48	41, 47	imbitrrdi 162	. . 3 $/\$ $/\$
49	5, 28, 48	mp2and 433	. 2
50		opeldmg 4928	. . 3 $/\$
51	1, 50	mpan 424	. 2
52	49, 51	mpd 13	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wceq 1395

wex 1538

wcel 2200

cab 2215

wral 2508

wrex 2509

cvv 2799

c0 3491

csn 3666

cop 3669

cuni 3888

con0 4454

csuc 4456

cdm 4719

cres 4721

wfn 5313

cfv 5318 recscrecs 6450

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 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-sbc 3029 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-br 4084 df-opab 4146 df-tr 4183 df-id 4384 df-iord 4457 df-on 4459 df-suc 4462 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-res 4731 df-iota 5278 df-fun 5320 df-fn 5321 df-fv 5326 df-recs 6451

This theorem is referenced by: tfr0 6469

W3C validator