Theorem limfillem2 14939

Description: Lemma for plimfil 14940.

Hypotheses

Ref	Expression
limfillem2.1	|- X = U.J
limfillem2.2	|- X = U.F

Assertion

Ref	Expression
limfillem2	|- ((J e. Top /\ F e. Fil) -> ((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F})

Distinct variable groups:   F,l   J,l   X,l

Proof of Theorem limfillem2

Step	Hyp	Ref	Expression
1		fveq2 4681	. . . . . 6 |- (J = if(J e. Top, J, {(/), {(/)}}) -> (fLim1` J) = (fLim1` if(J e. Top, J, {(/), {(/)}})))
2	1	fveq1d 4683	. . . . 5 |- (J = if(J e. Top, J, {(/), {(/)}}) -> ((fLim1` J)` F) = ((fLim1` if(J e. Top, J, {(/), {(/)}}))` F))
3		limfillem2.1	. . . . . . . 8 |- X = U.J
4		rabeq 2289	. . . . . . . 8 |- (X = U.J -> {l e. X | ((nei` J)` {l}) C_ F} = {l e. U.J | ((nei` J)` {l}) C_ F})
5	3, 4	ax-mp 7	. . . . . . 7 |- {l e. X | ((nei` J)` {l}) C_ F} = {l e. U.J | ((nei` J)` {l}) C_ F}
6	5	a1i 8	. . . . . 6 |- (J = if(J e. Top, J, {(/), {(/)}}) -> {l e. X | ((nei` J)` {l}) C_ F} = {l e. U.J | ((nei` J)` {l}) C_ F})
7		unieq 3185	. . . . . . 7 |- (J = if(J e. Top, J, {(/), {(/)}}) -> U.J = U.if(J e. Top, J, {(/), {(/)}}))
8		rabeq 2289	. . . . . . 7 |- (U.J = U.if(J e. Top, J, {(/), {(/)}}) -> {l e. U.J | ((nei` J)` {l}) C_ F} = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` J)` {l}) C_ F})
9	7, 8	syl 12	. . . . . 6 |- (J = if(J e. Top, J, {(/), {(/)}}) -> {l e. U.J | ((nei` J)` {l}) C_ F} = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` J)` {l}) C_ F})
10		fveq2 4681	. . . . . . . . 9 |- (J = if(J e. Top, J, {(/), {(/)}}) -> (nei` J) = (nei` if(J e. Top, J, {(/), {(/)}})))
11	10	fveq1d 4683	. . . . . . . 8 |- (J = if(J e. Top, J, {(/), {(/)}}) -> ((nei` J)` {l}) = ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}))
12	11	sseq1d 2644	. . . . . . 7 |- (J = if(J e. Top, J, {(/), {(/)}}) -> (((nei` J)` {l}) C_ F <-> ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F))
13	12	rabbidv 2287	. . . . . 6 |- (J = if(J e. Top, J, {(/), {(/)}}) -> {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` J)` {l}) C_ F} = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F})
14	6, 9, 13	3eqtrd 1929	. . . . 5 |- (J = if(J e. Top, J, {(/), {(/)}}) -> {l e. X | ((nei` J)` {l}) C_ F} = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F})
15	2, 14	eqeq12d 1899	. . . 4 |- (J = if(J e. Top, J, {(/), {(/)}}) -> (((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F} <-> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` F) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F}))
16	15	imbi2d 674	. . 3 |- (J = if(J e. Top, J, {(/), {(/)}}) -> ((F e. Fil -> ((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F}) <-> (F e. Fil -> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` F) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F})))
17		eleq1 1957	. . . 4 |- (F = if(J e. Top, F, {{(/)}}) -> (F e. Fil <-> if(J e. Top, F, {{(/)}}) e. Fil))
18		fveq2 4681	. . . . 5 |- (F = if(J e. Top, F, {{(/)}}) -> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` F) = ((fLim1` if(J e. Top, J, {(/), {(/)}}))` if(J e. Top, F, {{(/)}})))
19		sseq2 2639	. . . . . 6 |- (F = if(J e. Top, F, {{(/)}}) -> (((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F <-> ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ if(J e. Top, F, {{(/)}})))
20	19	rabbidv 2287	. . . . 5 |- (F = if(J e. Top, F, {{(/)}}) -> {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F} = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ if(J e. Top, F, {{(/)}})})
21	18, 20	eqeq12d 1899	. . . 4 |- (F = if(J e. Top, F, {{(/)}}) -> (((fLim1` if(J e. Top, J, {(/), {(/)}}))` F) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F} <-> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` if(J e. Top, F, {{(/)}})) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ if(J e. Top, F, {{(/)}})}))
22	17, 21	imbi12d 688	. . 3 |- (F = if(J e. Top, F, {{(/)}}) -> ((F e. Fil -> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` F) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ F}) <-> (if(J e. Top, F, {{(/)}}) e. Fil -> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` if(J e. Top, F, {{(/)}})) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ if(J e. Top, F, {{(/)}})})))
23		indistop 8918	. . . . 5 |- {(/), {(/)}} e. Top
24	23	elimel 3025	. . . 4 |- if(J e. Top, J, {(/), {(/)}}) e. Top
25		eqid 1884	. . . 4 |- U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, J, {(/), {(/)}})
26		iftrue 2989	. . . . . . 7 |- (J e. Top -> if(J e. Top, J, {(/), {(/)}}) = J)
27	26	eqcomd 1889	. . . . . 6 |- (J e. Top -> J = if(J e. Top, J, {(/), {(/)}}))
28		iftrue 2989	. . . . . . 7 |- (J e. Top -> if(J e. Top, F, {{(/)}}) = F)
29	28	eqcomd 1889	. . . . . 6 |- (J e. Top -> F = if(J e. Top, F, {{(/)}}))
30		limfillem2.2	. . . . . . . . . 10 |- X = U.F
31	30, 3	eqtr3i 1910	. . . . . . . . 9 |- U.F = U.J
32		eqtr 1904	. . . . . . . . . 10 |- ((U.F = U.J /\ U.J = U.if(J e. Top, J, {(/), {(/)}})) -> U.F = U.if(J e. Top, J, {(/), {(/)}}))
33		eqtr 1904	. . . . . . . . . . . 12 |- ((U.if(J e. Top, J, {(/), {(/)}}) = U.F /\ U.F = U.if(J e. Top, F, {{(/)}})) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
34	33	ex 402	. . . . . . . . . . 11 |- (U.if(J e. Top, J, {(/), {(/)}}) = U.F -> (U.F = U.if(J e. Top, F, {{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
35	34	eqcoms 1887	. . . . . . . . . 10 |- (U.F = U.if(J e. Top, J, {(/), {(/)}}) -> (U.F = U.if(J e. Top, F, {{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
36	32, 35	syl 12	. . . . . . . . 9 |- ((U.F = U.J /\ U.J = U.if(J e. Top, J, {(/), {(/)}})) -> (U.F = U.if(J e. Top, F, {{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
37	31, 36	mpan 759	. . . . . . . 8 |- (U.J = U.if(J e. Top, J, {(/), {(/)}}) -> (U.F = U.if(J e. Top, F, {{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
38	37	imp 377	. . . . . . 7 |- ((U.J = U.if(J e. Top, J, {(/), {(/)}}) /\ U.F = U.if(J e. Top, F, {{(/)}})) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
39		unieq 3185	. . . . . . 7 |- (F = if(J e. Top, F, {{(/)}}) -> U.F = U.if(J e. Top, F, {{(/)}}))
40	38, 7, 39	syl2an 503	. . . . . 6 |- ((J = if(J e. Top, J, {(/), {(/)}}) /\ F = if(J e. Top, F, {{(/)}})) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
41	27, 29, 40	syl11anc 524	. . . . 5 |- (J e. Top -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
42		iffalse 2991	. . . . . 6 |- (-. J e. Top -> if(J e. Top, J, {(/), {(/)}}) = {(/), {(/)}})
43		iffalse 2991	. . . . . 6 |- (-. J e. Top -> if(J e. Top, F, {{(/)}}) = {{(/)}})
44		0ex 3446	. . . . . . . . . 10 |- (/) e. _V
45		p0ex 3495	. . . . . . . . . 10 |- {(/)} e. _V
46	44, 45	unipr 3191	. . . . . . . . 9 |- U.{(/), {(/)}} = ((/) u. {(/)})
47		un0 2896	. . . . . . . . . 10 |- ({(/)} u. (/)) = {(/)}
48		uncom 2744	. . . . . . . . . 10 |- ((/) u. {(/)}) = ({(/)} u. (/))
49	45	unisn 3193	. . . . . . . . . 10 |- U.{{(/)}} = {(/)}
50	47, 48, 49	3eqtr4i 1921	. . . . . . . . 9 |- ((/) u. {(/)}) = U.{{(/)}}
51	46, 50	eqtri 1908	. . . . . . . 8 |- U.{(/), {(/)}} = U.{{(/)}}
52		eqtr 1904	. . . . . . . . . . 11 |- ((U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}} /\ U.{(/), {(/)}} = U.{{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.{{(/)}})
53		eqtr 1904	. . . . . . . . . . . . . 14 |- ((U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} /\ U.{{(/)}} = U.if(J e. Top, J, {(/), {(/)}})) -> U.if(J e. Top, F, {{(/)}}) = U.if(J e. Top, J, {(/), {(/)}}))
54	53	eqcomd 1889	. . . . . . . . . . . . 13 |- ((U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} /\ U.{{(/)}} = U.if(J e. Top, J, {(/), {(/)}})) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
55	54	expcom 403	. . . . . . . . . . . 12 |- (U.{{(/)}} = U.if(J e. Top, J, {(/), {(/)}}) -> (U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
56	55	eqcoms 1887	. . . . . . . . . . 11 |- (U.if(J e. Top, J, {(/), {(/)}}) = U.{{(/)}} -> (U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
57	52, 56	syl 12	. . . . . . . . . 10 |- ((U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}} /\ U.{(/), {(/)}} = U.{{(/)}}) -> (U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
58	57	expcom 403	. . . . . . . . 9 |- (U.{(/), {(/)}} = U.{{(/)}} -> (U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}} -> (U.if(J e. Top, F, {{(/)}}) = U.{{(/)}} -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))))
59	58	imp3a 388	. . . . . . . 8 |- (U.{(/), {(/)}} = U.{{(/)}} -> ((U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}} /\ U.if(J e. Top, F, {{(/)}}) = U.{{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})))
60	51, 59	ax-mp 7	. . . . . . 7 |- ((U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}} /\ U.if(J e. Top, F, {{(/)}}) = U.{{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
61		unieq 3185	. . . . . . 7 |- (if(J e. Top, J, {(/), {(/)}}) = {(/), {(/)}} -> U.if(J e. Top, J, {(/), {(/)}}) = U.{(/), {(/)}})
62		unieq 3185	. . . . . . 7 |- (if(J e. Top, F, {{(/)}}) = {{(/)}} -> U.if(J e. Top, F, {{(/)}}) = U.{{(/)}})
63	60, 61, 62	syl2an 503	. . . . . 6 |- ((if(J e. Top, J, {(/), {(/)}}) = {(/), {(/)}} /\ if(J e. Top, F, {{(/)}}) = {{(/)}}) -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
64	42, 43, 63	syl11anc 524	. . . . 5 |- (-. J e. Top -> U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}}))
65	41, 64	pm2.61i 140	. . . 4 |- U.if(J e. Top, J, {(/), {(/)}}) = U.if(J e. Top, F, {{(/)}})
66	24, 25, 65	limfillem1 14938	. . 3 |- (if(J e. Top, F, {{(/)}}) e. Fil -> ((fLim1` if(J e. Top, J, {(/), {(/)}}))` if(J e. Top, F, {{(/)}})) = {l e. U.if(J e. Top, J, {(/), {(/)}}) | ((nei` if(J e. Top, J, {(/), {(/)}}))` {l}) C_ if(J e. Top, F, {{(/)}})})
67	16, 22, 66	dedth2v 3018	. 2 |- (J e. Top -> (F e. Fil -> ((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F}))
68	67	imp 377	1 |- ((J e. Top /\ F e. Fil) -> ((fLim1` J)` F) = {l e. X | ((nei` J)` {l}) C_ F})

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  {crab 2108   u. cun 2591   C_ wss 2593  (/)c0 2875  ifcif 2982  {csn 3044  {cpr 3045  U.cuni 3177  ` cfv 3998  Topctop 8857  neicnei 8988  Filcfil 10264  fLim1cflim1 10294

This theorem is referenced by:  plimfil 14940

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-top 8861  df-flim1 10295

Copyright terms: Public domain