finxpreclem2 - Mathbox for ML

	Mathbox for ML		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > finxpreclem2		Structured version Visualization version Unicode version

Theorem finxpreclem2 31794

Description: Lemma for

recursion theorems. (Contributed by ML, 17-Oct-2020.)

**Assertion**
Ref	Expression
finxpreclem2	$/\$ $/\$

Distinct variable groups:

**Proof of Theorem finxpreclem2**
Step	Hyp	Ref	Expression
1		nfv 1763	. . . . . 6 $/\$
2		nfmpt22 6364	. . . . . . . 8 $/\$
3		nfcv 2594	. . . . . . . 8
4	2, 3	nffv 5877	. . . . . . 7 $/\$
5		nfcv 2594	. . . . . . 7
6	4, 5	nfne 2725	. . . . . 6 $/\$
7	1, 6	nfim 2005	. . . . 5 $/\$ $/\$
8		nfv 1763	. . . . . . 7
9		nfv 1763	. . . . . . . 8 $/\$
10		nfmpt21 6363	. . . . . . . . . 10 $/\$
11		nfcv 2594	. . . . . . . . . 10
12	10, 11	nffv 5877	. . . . . . . . 9 $/\$
13		nfcv 2594	. . . . . . . . 9
14	12, 13	nfne 2725	. . . . . . . 8 $/\$
15	9, 14	nfim 2005	. . . . . . 7 $/\$ $/\$
16	8, 15	nfim 2005	. . . . . 6 $/\$ $/\$
17		1onn 7345	. . . . . . 7
18	17	elexi 3057	. . . . . 6
19		df-ov 6298	. . . . . . . . . 10 $/\$ $/\$
20		0ex 4538	. . . . . . . . . . . . . . . 16
21		opex 4667	. . . . . . . . . . . . . . . . 17
22		opex 4667	. . . . . . . . . . . . . . . . 17
23	21, 22	ifex 3951	. . . . . . . . . . . . . . . 16
24	20, 23	ifex 3951	. . . . . . . . . . . . . . 15 $/\$
25	24	csbex 4541	. . . . . . . . . . . . . 14 $/\$
26	25	csbex 4541	. . . . . . . . . . . . 13 $/\$
27		eqid 2453	. . . . . . . . . . . . . 14 $/\$ $/\$
28	27	ovmpt2s 6425	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
29	17, 26, 28	mp3an13 1357	. . . . . . . . . . . 12 $/\$ $/\$
30	29	adantr 467	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
31		csbeq1a 3374	. . . . . . . . . . . . . . 15 $/\$ $/\$
32		csbeq1a 3374	. . . . . . . . . . . . . . 15 $/\$ $/\$
33	31, 32	sylan9eqr 2509	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
34	33	adantl 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
35		eleq1 2519	. . . . . . . . . . . . . . . . . . . 20
36	35	notbid 296	. . . . . . . . . . . . . . . . . . 19
37	36	biimprcd 229	. . . . . . . . . . . . . . . . . 18
38		pm3.14 505	. . . . . . . . . . . . . . . . . . 19 $\/$ $/\$
39	38	olcs 397	. . . . . . . . . . . . . . . . . 18 $/\$
40	37, 39	syl6 34	. . . . . . . . . . . . . . . . 17 $/\$
41		iffalse 3892	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
42	40, 41	syl6 34	. . . . . . . . . . . . . . . 16 $/\$
43	42	imp 431	. . . . . . . . . . . . . . 15 $/\$ $/\$
44		ifeqor 3927	. . . . . . . . . . . . . . . . 17 $\/$
45		vex 3050	. . . . . . . . . . . . . . . . . . . . . 22
46	45	uniex 6592	. . . . . . . . . . . . . . . . . . . . 21
47		fvex 5880	. . . . . . . . . . . . . . . . . . . . 21
48	46, 47	opnzi 4677	. . . . . . . . . . . . . . . . . . . 20
49	48	neii 2628	. . . . . . . . . . . . . . . . . . 19
50		eqeq1 2457	. . . . . . . . . . . . . . . . . . 19
51	49, 50	mtbiri 305	. . . . . . . . . . . . . . . . . 18
52		vex 3050	. . . . . . . . . . . . . . . . . . . . 21
53	45, 52	opnzi 4677	. . . . . . . . . . . . . . . . . . . 20
54	53	neii 2628	. . . . . . . . . . . . . . . . . . 19
55		eqeq1 2457	. . . . . . . . . . . . . . . . . . 19
56	54, 55	mtbiri 305	. . . . . . . . . . . . . . . . . 18
57	51, 56	jaoi 381	. . . . . . . . . . . . . . . . 17 $\/$
58	44, 57	mp1i 13	. . . . . . . . . . . . . . . 16 $/\$
59	58	neqned 2633	. . . . . . . . . . . . . . 15 $/\$
60	43, 59	eqnetrd 2693	. . . . . . . . . . . . . 14 $/\$ $/\$
61	60	adantrl 723	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
62	34, 61	eqnetrrd 2694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
63	62	adantl 468	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
64	30, 63	eqnetrd 2693	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
65	19, 64	syl5eqner 2701	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
66	65	ancom2s 812	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
67	66	an12s 811	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
68	67	exp31 609	. . . . . 6 $/\$ $/\$
69	16, 18, 68	vtoclef 3124	. . . . 5 $/\$ $/\$
70	7, 69	vtoclefex 31748	. . . 4 $/\$ $/\$
71	70	anabsi5 827	. . 3 $/\$ $/\$
72	71	necomd 2681	. 2 $/\$ $/\$
73	72	neneqd 2631	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 370 $/\$ wa 371

wceq 1446

wcel 1889

wne 2624

cvv 3047

csb 3365

c0 3733

cif 3883

cop 3976

cuni 4201

cxp 4835

cfv 5585 (class class class)co 6295

cmpt2 6297

com 6697

c1st 6796

c1o 7180

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-fal 1452 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-tr 4501 df-eprel 4748 df-id 4752 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-ord 5429 df-on 5430 df-lim 5431 df-suc 5432 df-iota 5549 df-fun 5587 df-fv 5593 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-om 6698 df-1o 7187

This theorem is referenced by: finxp1o 31796

W3C validator