Theorem ltfintrilem1 4466

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

Assertion

Ref	Expression
ltfintrilem1	|- {m | (n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))} e. _V

Distinct variable group:   m,n

Proof of Theorem ltfintrilem1

Dummy variable t is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unab 3522	. . 3 |- ({m | -. n e. Nn } u. {m | (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))}) = {m | (-. n e. Nn \/ (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))}
2		df-sn 3742	. . . . . 6 |- {(/)} = {m | m = (/)}
3		elun 3221	. . . . . . . . . 10 |- (m e. ((`'k <fin "k{n}) u. {n}) <-> (m e. (`'k <fin "k{n}) \/ m e. {n}))
4		vex 2863	. . . . . . . . . . . . . 14 |- m e. _V
5	4	elimak 4260	. . . . . . . . . . . . 13 |- (m e. (`'k <fin "k{n}) <-> E.t e. {n}<<t, m>> e. `'k <fin )
6		vex 2863	. . . . . . . . . . . . . 14 |- n e. _V
7		opkeq1 4060	. . . . . . . . . . . . . . 15 |- (t = n -> <<t, m>> = <<n, m>>)
8	7	eleq1d 2419	. . . . . . . . . . . . . 14 |- (t = n -> (<<t, m>> e. `'k <fin <-> <<n, m>> e. `'k <fin ))
9	6, 8	rexsn 3769	. . . . . . . . . . . . 13 |- (E.t e. {n}<<t, m>> e. `'k <fin <-> <<n, m>> e. `'k <fin )
10	5, 9	bitri 240	. . . . . . . . . . . 12 |- (m e. (`'k <fin "k{n}) <-> <<n, m>> e. `'k <fin )
11	6, 4	opkelcnvk 4251	. . . . . . . . . . . 12 |- (<<n, m>> e. `'k <fin <-> <<m, n>> e. <fin )
12	10, 11	bitri 240	. . . . . . . . . . 11 |- (m e. (`'k <fin "k{n}) <-> <<m, n>> e. <fin )
13	4	elsnc 3757	. . . . . . . . . . 11 |- (m e. {n} <-> m = n)
14	12, 13	orbi12i 507	. . . . . . . . . 10 |- ((m e. (`'k <fin "k{n}) \/ m e. {n}) <-> (<<m, n>> e. <fin \/ m = n))
15	3, 14	bitri 240	. . . . . . . . 9 |- (m e. ((`'k <fin "k{n}) u. {n}) <-> (<<m, n>> e. <fin \/ m = n))
16	4	elimak 4260	. . . . . . . . . 10 |- (m e. ( <fin "k{n}) <-> E.t e. {n}<<t, m>> e. <fin )
17	7	eleq1d 2419	. . . . . . . . . . 11 |- (t = n -> (<<t, m>> e. <fin <-> <<n, m>> e. <fin ))
18	6, 17	rexsn 3769	. . . . . . . . . 10 |- (E.t e. {n}<<t, m>> e. <fin <-> <<n, m>> e. <fin )
19	16, 18	bitri 240	. . . . . . . . 9 |- (m e. ( <fin "k{n}) <-> <<n, m>> e. <fin )
20	15, 19	orbi12i 507	. . . . . . . 8 |- ((m e. ((`'k <fin "k{n}) u. {n}) \/ m e. ( <fin "k{n})) <-> ((<<m, n>> e. <fin \/ m = n) \/ <<n, m>> e. <fin ))
21		elun 3221	. . . . . . . 8 |- (m e. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})) <-> (m e. ((`'k <fin "k{n}) u. {n}) \/ m e. ( <fin "k{n})))
22		df-3or 935	. . . . . . . 8 |- ((<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ) <-> ((<<m, n>> e. <fin \/ m = n) \/ <<n, m>> e. <fin ))
23	20, 21, 22	3bitr4i 268	. . . . . . 7 |- (m e. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})) <-> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))
24	23	abbi2i 2465	. . . . . 6 |- (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})) = {m | (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )}
25	2, 24	uneq12i 3417	. . . . 5 |- ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n}))) = ({m | m = (/)} u. {m | (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )})
26		unab 3522	. . . . 5 |- ({m | m = (/)} u. {m | (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )}) = {m | (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))}
27	25, 26	eqtri 2373	. . . 4 |- ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n}))) = {m | (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))}
28	27	uneq2i 3416	. . 3 |- ({m | -. n e. Nn } u. ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})))) = ({m | -. n e. Nn } u. {m | (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))})
29		imor 401	. . . . 5 |- ((n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))) <-> (-. n e. Nn \/ (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))))
30		df-ne 2519	. . . . . . . 8 |- (m =/= (/) <-> -. m = (/))
31	30	imbi1i 315	. . . . . . 7 |- ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) <-> (-. m = (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))
32		df-or 359	. . . . . . 7 |- ((m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) <-> (-. m = (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))
33	31, 32	bitr4i 243	. . . . . 6 |- ((m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )) <-> (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))
34	33	orbi2i 505	. . . . 5 |- ((-. n e. Nn \/ (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))) <-> (-. n e. Nn \/ (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))))
35	29, 34	bitri 240	. . . 4 |- ((n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))) <-> (-. n e. Nn \/ (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin ))))
36	35	abbii 2466	. . 3 |- {m | (n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))} = {m | (-. n e. Nn \/ (m = (/) \/ (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))}
37	1, 28, 36	3eqtr4i 2383	. 2 |- ({m | -. n e. Nn } u. ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})))) = {m | (n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))}
38		abexv 4325	. . 3 |- {m | -. n e. Nn } e. _V
39		snex 4112	. . . 4 |- {(/)} e. _V
40		ltfinex 4465	. . . . . . . 8 |- <fin e. _V
41	40	cnvkex 4288	. . . . . . 7 |- `'k <fin e. _V
42		snex 4112	. . . . . . 7 |- {n} e. _V
43	41, 42	imakex 4301	. . . . . 6 |- (`'k <fin "k{n}) e. _V
44	43, 42	unex 4107	. . . . 5 |- ((`'k <fin "k{n}) u. {n}) e. _V
45	40, 42	imakex 4301	. . . . 5 |- ( <fin "k{n}) e. _V
46	44, 45	unex 4107	. . . 4 |- (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})) e. _V
47	39, 46	unex 4107	. . 3 |- ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n}))) e. _V
48	38, 47	unex 4107	. 2 |- ({m | -. n e. Nn } u. ({(/)} u. (((`'k <fin "k{n}) u. {n}) u. ( <fin "k{n})))) e. _V
49	37, 48	eqeltrri 2424	1 |- {m | (n e. Nn -> (m =/= (/) -> (<<m, n>> e. <fin \/ m = n \/ <<n, m>> e. <fin )))} e. _V

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   \/ w3o 933   = wceq 1642   e. wcel 1710  {cab 2339   =/= wne 2517  E.wrex 2616  _Vcvv 2860   u. cun 3208  (/)c0 3551  {csn 3738  <<copk 4058  `'_kccnvk 4176  "_kcimak 4180   Nn cnnc 4374   <_fin cltfin 4434

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 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

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 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-addc 4379  df-nnc 4380  df-ltfin 4442

This theorem is referenced by:  ltfintri  4467