tfr0dm - Intuitionistic Logic Explorer

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

Theorem tfr0dm 6389

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 4161	. . . . 5
2		opexg 4262	. . . . 5 $/\$
3	1, 2	mpan 424	. . . 4
4		snidg 3652	. . . 4
5	3, 4	syl 14	. . 3
6		fnsng 5306	. . . . 5 $/\$
7	1, 6	mpan 424	. . . 4
8		fvsng 5761	. . . . . . 7 $/\$
9	1, 8	mpan 424	. . . . . 6
10		res0 4951	. . . . . . 7
11	10	fveq2i 5564	. . . . . 6
12	9, 11	eqtr4di 2247	. . . . 5
13		fveq2 5561	. . . . . . 7
14		reseq2 4942	. . . . . . . 8
15	14	fveq2d 5565	. . . . . . 7
16	13, 15	eqeq12d 2211	. . . . . 6
17	1, 16	ralsn 3666	. . . . 5
18	12, 17	sylibr 134	. . . 4
19		suc0 4447	. . . . . 6
20		0elon 4428	. . . . . . 7
21	20	onsuci 4553	. . . . . 6
22	19, 21	eqeltrri 2270	. . . . 5
23		fneq2 5348	. . . . . . 7
24		raleq 2693	. . . . . . 7
25	23, 24	anbi12d 473	. . . . . 6 $/\$ $/\$
26	25	rspcev 2868	. . . . 5 $/\$ $/\$ $/\$
27	22, 26	mpan 424	. . . 4 $/\$ $/\$
28	7, 18, 27	syl2anc 411	. . 3 $/\$
29		snexg 4218	. . . . 5
30		eleq2 2260	. . . . . . 7
31		fneq1 5347	. . . . . . . . 9
32		fveq1 5560	. . . . . . . . . . 11
33		reseq1 4941	. . . . . . . . . . . 12
34	33	fveq2d 5565	. . . . . . . . . . 11
35	32, 34	eqeq12d 2211	. . . . . . . . . 10
36	35	ralbidv 2497	. . . . . . . . 9
37	31, 36	anbi12d 473	. . . . . . . 8 $/\$ $/\$
38	37	rexbidv 2498	. . . . . . 7 $/\$ $/\$
39	30, 38	anbi12d 473	. . . . . 6 $/\$ $/\$ $/\$ $/\$
40	39	spcegv 2852	. . . . 5 $/\$ $/\$ $/\$ $/\$
41	3, 29, 40	3syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$
42		tfr.1	. . . . . 6 recs
43	42	eleq2i 2263	. . . . 5 recs
44		df-recs 6372	. . . . . 6 recs $/\$
45	44	eleq2i 2263	. . . . 5 recs $/\$
46		eluniab 3852	. . . . 5 $/\$ $/\$ $/\$
47	43, 45, 46	3bitri 206	. . . 4 $/\$ $/\$
48	41, 47	imbitrrdi 162	. . 3 $/\$ $/\$
49	5, 28, 48	mp2and 433	. 2
50		opeldmg 4872	. . 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 1364

wex 1506

wcel 2167

cab 2182

wral 2475

wrex 2476

cvv 2763

c0 3451

csn 3623

cop 3626

cuni 3840

con0 4399

csuc 4401

cdm 4664

cres 4666

wfn 5254

cfv 5259 recscrecs 6371

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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-nul 4160 ax-pow 4208 ax-pr 4243 ax-un 4469

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 df-rex 2481 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3452 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-br 4035 df-opab 4096 df-tr 4133 df-id 4329 df-iord 4402 df-on 4404 df-suc 4407 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-res 4676 df-iota 5220 df-fun 5261 df-fn 5262 df-fv 5267 df-recs 6372

This theorem is referenced by: tfr0 6390

W3C validator