ltfintrilem1 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > ltfintrilem1		Unicode version

Theorem ltfintrilem1 4465

Description: Lemma for ltfintri 4466. Establish stratification for induction. (Contributed by SF, 29-Jan-2015.)

**Assertion**
Ref	Expression
ltfintrilem1	Nn _fin $\/$ $\/$ _fin

Distinct variable group:

Proof of Theorem ltfintrilem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unab 3521	. . 3 Nn $\/$ _fin $\/$ $\/$ _fin Nn $\/$ $\/$ _fin $\/$ $\/$ _fin
2		df-sn 3741	. . . . . 6
3		elun 3220	. . . . . . . . . 10 _k _fin _k _k _fin _k $\/$
4		vex 2862	. . . . . . . . . . . . . 14
5	4	elimak 4259	. . . . . . . . . . . . 13 _k _fin _k _k _fin
6		vex 2862	. . . . . . . . . . . . . 14
7		opkeq1 4059	. . . . . . . . . . . . . . 15
8	7	eleq1d 2419	. . . . . . . . . . . . . 14 _k _fin _k _fin
9	6, 8	rexsn 3768	. . . . . . . . . . . . 13 _k _fin _k _fin
10	5, 9	bitri 240	. . . . . . . . . . . 12 _k _fin _k _k _fin
11	6, 4	opkelcnvk 4250	. . . . . . . . . . . 12 _k _fin _fin
12	10, 11	bitri 240	. . . . . . . . . . 11 _k _fin _k _fin
13	4	elsnc 3756	. . . . . . . . . . 11
14	12, 13	orbi12i 507	. . . . . . . . . 10 _k _fin _k $\/$ _fin $\/$
15	3, 14	bitri 240	. . . . . . . . 9 _k _fin _k _fin $\/$
16	4	elimak 4259	. . . . . . . . . 10 _fin _k _fin
17	7	eleq1d 2419	. . . . . . . . . . 11 _fin _fin
18	6, 17	rexsn 3768	. . . . . . . . . 10 _fin _fin
19	16, 18	bitri 240	. . . . . . . . 9 _fin _k _fin
20	15, 19	orbi12i 507	. . . . . . . 8 _k _fin _k $\/$ _fin _k _fin $\/$ $\/$ _fin
21		elun 3220	. . . . . . . 8 _k _fin _k _fin _k _k _fin _k $\/$ _fin _k
22		df-3or 935	. . . . . . . 8 _fin $\/$ $\/$ _fin _fin $\/$ $\/$ _fin
23	20, 21, 22	3bitr4i 268	. . . . . . 7 _k _fin _k _fin _k _fin $\/$ $\/$ _fin
24	23	abbi2i 2464	. . . . . 6 _k _fin _k _fin _k _fin $\/$ $\/$ _fin
25	2, 24	uneq12i 3416	. . . . 5 _k _fin _k _fin _k _fin $\/$ $\/$ _fin
26		unab 3521	. . . . 5 _fin $\/$ $\/$ _fin $\/$ _fin $\/$ $\/$ _fin
27	25, 26	eqtri 2373	. . . 4 _k _fin _k _fin _k $\/$ _fin $\/$ $\/$ _fin
28	27	uneq2i 3415	. . 3 Nn _k _fin _k _fin _k Nn $\/$ _fin $\/$ $\/$ _fin
29		imor 401	. . . . 5 Nn _fin $\/$ $\/$ _fin Nn $\/$ _fin $\/$ $\/$ _fin
30		df-ne 2518	. . . . . . . 8
31	30	imbi1i 315	. . . . . . 7 _fin $\/$ $\/$ _fin _fin $\/$ $\/$ _fin
32		df-or 359	. . . . . . 7 $\/$ _fin $\/$ $\/$ _fin _fin $\/$ $\/$ _fin
33	31, 32	bitr4i 243	. . . . . 6 _fin $\/$ $\/$ _fin $\/$ _fin $\/$ $\/$ _fin
34	33	orbi2i 505	. . . . 5 Nn $\/$ _fin $\/$ $\/$ _fin Nn $\/$ $\/$ _fin $\/$ $\/$ _fin
35	29, 34	bitri 240	. . . 4 Nn _fin $\/$ $\/$ _fin Nn $\/$ $\/$ _fin $\/$ $\/$ _fin
36	35	abbii 2465	. . 3 Nn _fin $\/$ $\/$ _fin Nn $\/$ $\/$ _fin $\/$ $\/$ _fin
37	1, 28, 36	3eqtr4i 2383	. 2 Nn _k _fin _k _fin _k Nn _fin $\/$ $\/$ _fin
38		abexv 4324	. . 3 Nn
39		snex 4111	. . . 4
40		ltfinex 4464	. . . . . . . 8 _fin
41	40	cnvkex 4287	. . . . . . 7 _k _fin
42		snex 4111	. . . . . . 7
43	41, 42	imakex 4300	. . . . . 6 _k _fin _k
44	43, 42	unex 4106	. . . . 5 _k _fin _k
45	40, 42	imakex 4300	. . . . 5 _fin _k
46	44, 45	unex 4106	. . . 4 _k _fin _k _fin _k
47	39, 46	unex 4106	. . 3 _k _fin _k _fin _k
48	38, 47	unex 4106	. 2 Nn _k _fin _k _fin _k
49	37, 48	eqeltrri 2424	1 Nn _fin $\/$ $\/$ _fin

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $\/$ wo 357 $\/$ w3o 933

wceq 1642

wcel 1710

cab 2339

wne 2516

wrex 2615

cvv 2859

cun 3207

c0 3550

csn 3737

copk 4057

_kccnvk 4175

_kcimak 4179 Nn cnnc 4373

_fin cltfin 4433

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-addc 4378 df-nnc 4379 df-ltfin 4441

This theorem is referenced by: ltfintri 4466

W3C validator