Theorem filnet 15645

Description: A filter has the same convergence and clustering properties as some net.

Hypothesis

Ref	Expression
filnet.1	|- X = U.F

Assertion

Ref	Expression
filnet	|- (F e. Fil -> E.d e. Dir E.f(f:dom d-->X /\ F = ((X FilMap ran (tail` d))` f)))

Distinct variable groups:   f,d,F   X,d,f

Proof of Theorem filnet

Step	Hyp	Ref	Expression
1		filnet.1	. . 3 |- X = U.F
2	1	filnetlem4 15643	. 2 |- (F e. Fil -> {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir)
3		fo1st 5032	. . . . . 6 |- 1st:_V-onto->_V
4		fofun 4618	. . . . . 6 |- (1st:_V-onto->_V -> Fun 1st)
5	3, 4	ax-mp 7	. . . . 5 |- Fun 1st
6	5	a1i 8	. . . 4 |- (F e. Fil -> Fun 1st)
7		uniexg 3795	. . . . . . 7 |- (F e. Fil -> U.F e. _V)
8	7, 1	syl5eqel 1975	. . . . . 6 |- (F e. Fil -> X e. _V)
9		xpexg 4095	. . . . . . 7 |- ((X e. _V /\ F e. Fil) -> (X X. F) e. _V)
10		xpexg 4095	. . . . . . 7 |- (((X X. F) e. _V /\ (X X. F) e. _V) -> ((X X. F) X. (X X. F)) e. _V)
11	9, 9, 10	syl11anc 524	. . . . . 6 |- ((X e. _V /\ F e. Fil) -> ((X X. F) X. (X X. F)) e. _V)
12	8, 11	mpancom 769	. . . . 5 |- (F e. Fil -> ((X X. F) X. (X X. F)) e. _V)
13		eleq1 1957	. . . . . . . . . . . . . 14 |- (x = <.u, h>. -> (x e. (X X. F) <-> <.u, h>. e. (X X. F)))
14		eleq1 1957	. . . . . . . . . . . . . 14 |- (y = <.v, g>. -> (y e. (X X. F) <-> <.v, g>. e. (X X. F)))
15	13, 14	bi2anan9 694	. . . . . . . . . . . . 13 |- ((x = <.u, h>. /\ y = <.v, g>.) -> ((x e. (X X. F) /\ y e. (X X. F)) <-> (<.u, h>. e. (X X. F) /\ <.v, g>. e. (X X. F))))
16		opelxpi 4040	. . . . . . . . . . . . . . 15 |- ((u e. X /\ h e. F) -> <.u, h>. e. (X X. F))
17	16	ad2ant2r 445	. . . . . . . . . . . . . 14 |- (((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) -> <.u, h>. e. (X X. F))
18		opelxpi 4040	. . . . . . . . . . . . . . 15 |- ((v e. X /\ g e. F) -> <.v, g>. e. (X X. F))
19	18	ad2ant2l 444	. . . . . . . . . . . . . 14 |- (((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) -> <.v, g>. e. (X X. F))
20	17, 19	jca 310	. . . . . . . . . . . . 13 |- (((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) -> (<.u, h>. e. (X X. F) /\ <.v, g>. e. (X X. F)))
21	15, 20	syl5cbir 228	. . . . . . . . . . . 12 |- (((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) -> ((x = <.u, h>. /\ y = <.v, g>.) -> (x e. (X X. F) /\ y e. (X X. F))))
22	21	adantrd 427	. . . . . . . . . . 11 |- (((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) -> (((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> (x e. (X X. F) /\ y e. (X X. F))))
23	22	ex 402	. . . . . . . . . 10 |- ((u e. X /\ v e. X) -> ((h e. F /\ g e. F) -> (((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> (x e. (X X. F) /\ y e. (X X. F)))))
24	23	r19.23advv 2218	. . . . . . . . 9 |- ((u e. X /\ v e. X) -> (E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> (x e. (X X. F) /\ y e. (X X. F))))
25	24	r19.23aivv 2217	. . . . . . . 8 |- (E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> (x e. (X X. F) /\ y e. (X X. F)))
26	25	ssopab2i 3574	. . . . . . 7 |- {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ {<.x, y>. | (x e. (X X. F) /\ y e. (X X. F))}
27		df-xp 4000	. . . . . . 7 |- ((X X. F) X. (X X. F)) = {<.x, y>. | (x e. (X X. F) /\ y e. (X X. F))}
28	26, 27	sseqtr4i 2650	. . . . . 6 |- {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ ((X X. F) X. (X X. F))
29		ssexg 3457	. . . . . 6 |- (({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ ((X X. F) X. (X X. F)) /\ ((X X. F) X. (X X. F)) e. _V) -> {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V)
30	28, 29	mpan 759	. . . . 5 |- (((X X. F) X. (X X. F)) e. _V -> {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V)
31		dmexg 4206	. . . . 5 |- ({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V)
32	12, 30, 31	3syl 24	. . . 4 |- (F e. Fil -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V)
33		resfunexg 4500	. . . 4 |- ((Fun 1st /\ dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. _V) -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. _V)
34	6, 32, 33	syl11anc 524	. . 3 |- (F e. Fil -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. _V)
35		ssv 2636	. . . . . . . 8 |- dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ _V
36		fofn 4619	. . . . . . . . . 10 |- (1st:_V-onto->_V -> 1st Fn _V)
37	3, 36	ax-mp 7	. . . . . . . . 9 |- 1st Fn _V
38		fnssresb 4525	. . . . . . . . 9 |- (1st Fn _V -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} <-> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ _V))
39	37, 38	ax-mp 7	. . . . . . . 8 |- ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} <-> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ _V)
40	35, 39	mpbir 207	. . . . . . 7 |- (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}
41	40	a1i 8	. . . . . 6 |- (F e. Fil -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
42		dmss 4156	. . . . . . . . . . . 12 |- ({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ ((X X. F) X. (X X. F)) -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ dom ((X X. F) X. (X X. F)))
43	28, 42	ax-mp 7	. . . . . . . . . . 11 |- dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ dom ((X X. F) X. (X X. F))
44		dmxpid 4179	. . . . . . . . . . 11 |- dom ((X X. F) X. (X X. F)) = (X X. F)
45	43, 44	sseqtri 2649	. . . . . . . . . 10 |- dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ (X X. F)
46	45	a1i 8	. . . . . . . . 9 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ (X X. F))
47		ssres2 4240	. . . . . . . . 9 |- (dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} C_ (X X. F) -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ (1st |` (X X. F)))
48		rnss 4189	. . . . . . . . 9 |- ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ (1st |` (X X. F)) -> ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ ran (1st |` (X X. F)))
49	46, 47, 48	3syl 24	. . . . . . . 8 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ ran (1st |` (X X. F)))
50		f1stres 5034	. . . . . . . . . 10 |- (1st |` (X X. F)):(X X. F)-->X
51		frn 4569	. . . . . . . . . 10 |- ((1st |` (X X. F)):(X X. F)-->X -> ran (1st |` (X X. F)) C_ X)
52	50, 51	ax-mp 7	. . . . . . . . 9 |- ran (1st |` (X X. F)) C_ X
53	52	a1i 8	. . . . . . . 8 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ran (1st |` (X X. F)) C_ X)
54	49, 53	sstrd 2627	. . . . . . 7 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ X)
55	54	ex 402	. . . . . 6 |- (F e. Fil -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ X))
56	41, 55	jcai 313	. . . . 5 |- (F e. Fil -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} /\ ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ X))
57		df-f 4010	. . . . 5 |- ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X <-> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} /\ ran (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) C_ X))
58	56, 57	sylibr 217	. . . 4 |- (F e. Fil -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X)
59		elssuni 3206	. . . . . . . . . . . 12 |- (t e. F -> t C_ U.F)
60	59, 1	syl6ssr 2664	. . . . . . . . . . 11 |- (t e. F -> t C_ X)
61	60	a1i 8	. . . . . . . . . 10 |- (F e. Fil -> (t e. F -> t C_ X))
62		eleq1 1957	. . . . . . . . . . . . . . 15 |- (t = (/) -> (t e. F <-> (/) e. F))
63	62	notbid 673	. . . . . . . . . . . . . 14 |- (t = (/) -> (-. t e. F <-> -. (/) e. F))
64		filesn 10268	. . . . . . . . . . . . . 14 |- (F e. Fil -> -. (/) e. F)
65	63, 64	syl5cbir 228	. . . . . . . . . . . . 13 |- (F e. Fil -> (t = (/) -> -. t e. F))
66	65	necon2ad 2055	. . . . . . . . . . . 12 |- (F e. Fil -> (t e. F -> t =/= (/)))
67		n0 2884	. . . . . . . . . . . 12 |- (t =/= (/) <-> E.d d e. t)
68	66, 67	syl6ib 229	. . . . . . . . . . 11 |- (F e. Fil -> (t e. F -> E.d d e. t))
69		eqid 1884	. . . . . . . . . . . . . . . . . . 19 |- dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}
70	69	tailmap 15636	. . . . . . . . . . . . . . . . . 18 |- ({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
71		ffn 4562	. . . . . . . . . . . . . . . . . 18 |- ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
72	2, 70, 71	3syl 24	. . . . . . . . . . . . . . . . 17 |- (F e. Fil -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
73	72	adantr 425	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
74		simpr 350	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (t e. F /\ d e. t))
75		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- d e. _V
76		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- t e. _V
77		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (m = d -> (m e. n <-> d e. n))
78	77	anbi2d 678	. . . . . . . . . . . . . . . . . . 19 |- (m = d -> ((n e. F /\ m e. n) <-> (n e. F /\ d e. n)))
79		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (n = t -> (n e. F <-> t e. F))
80		eleq2 1958	. . . . . . . . . . . . . . . . . . . 20 |- (n = t -> (d e. n <-> d e. t))
81	79, 80	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (n = t -> ((n e. F /\ d e. n) <-> (t e. F /\ d e. t)))
82	75, 76, 78, 81	opelopab 3570	. . . . . . . . . . . . . . . . . 18 |- (<.d, t>. e. {<.m, n>. | (n e. F /\ m e. n)} <-> (t e. F /\ d e. t))
83	74, 82	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> <.d, t>. e. {<.m, n>. | (n e. F /\ m e. n)})
84		dirdm 10354	. . . . . . . . . . . . . . . . . . . . 21 |- ({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = U.U.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
85	2, 84	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = U.U.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
86	1	filnetlem1 15640	. . . . . . . . . . . . . . . . . . . 20 |- U.U.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = {<.m, n>. | (n e. F /\ m e. n)}
87	85, 86	syl6eq 1944	. . . . . . . . . . . . . . . . . . 19 |- (F e. Fil -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = {<.m, n>. | (n e. F /\ m e. n)})
88	87	eleq2d 1964	. . . . . . . . . . . . . . . . . 18 |- (F e. Fil -> (<.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} <-> <.d, t>. e. {<.m, n>. | (n e. F /\ m e. n)}))
89	88	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (<.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} <-> <.d, t>. e. {<.m, n>. | (n e. F /\ m e. n)}))
90	83, 89	mpbird 213	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> <.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
91		fnfvelrn 4786	. . . . . . . . . . . . . . . 16 |- (((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) Fn dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} /\ <.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))
92	73, 90, 91	syl11anc 524	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))
93	2, 70	syl 12	. . . . . . . . . . . . . . . . . . . . . 22 |- (F e. Fil -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
94	93	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
95		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . 21 |- (((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} /\ <.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
96	94, 90, 95	syl11anc 524	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
97		fvex 4689	. . . . . . . . . . . . . . . . . . . . 21 |- ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. _V
98	97	elpw 3037	. . . . . . . . . . . . . . . . . . . 20 |- (((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ~Pdom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} <-> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) C_ dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
99	96, 98	sylib 215	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) C_ dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
100		resabs1 4244	. . . . . . . . . . . . . . . . . . 19 |- (((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) C_ dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) = (1st |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)))
101	99, 100	syl 12	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) = (1st |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)))
102	101	rneqd 4188	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ran ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) = ran (1st |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)))
103	2	adantr 425	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir)
104		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- o e. _V
105	69	eltail 15635	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir /\ <.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} /\ o e. _V) -> (o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) <-> <.d, t>.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}o))
106	104, 105	mp3an3 1180	. . . . . . . . . . . . . . . . . . . . . . 23 |- (({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir /\ <.d, t>. e. dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> (o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) <-> <.d, t>.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}o))
107	103, 90, 106	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) <-> <.d, t>.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}o))
108		simpr3 884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> g C_ h)
109	108	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> g C_ h)
110		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> (1st` o) = f)
111		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> o = <.v, g>.)
112	111	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> (1st` o) = (1st` <.v, g>.))
113	112	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> (1st` o) = (1st` <.v, g>.))
114		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- v e. _V
115	114	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (1st` <.v, g>.) = v
116	113, 115	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> (1st` o) = v)
117	110, 116	eqtr3d 1927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> f = v)
118		simpr2 883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> v e. g)
119	118	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> v e. g)
120	117, 119	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> f e. g)
121	109, 120	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> f e. h)
122		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- h e. _V
123	76, 122	opth2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (<.d, t>. = <.u, h>. -> t = h)
124	123	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> t = h)
125	124	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> t = h)
126	121, 125	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))) /\ ((F e. Fil /\ (t e. F /\ d e. t)) /\ (1st` o) = f)) -> f e. t)
127	126	exp56 15341	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((u e. X /\ v e. X) -> ((h e. F /\ g e. F) -> (((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t e. F /\ d e. t)) -> ((1st` o) = f -> f e. t)))))
128	127	r19.23advv 2218	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u e. X /\ v e. X) -> (E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t e. F /\ d e. t)) -> ((1st` o) = f -> f e. t))))
129	128	r19.23aivv 2217	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t e. F /\ d e. t)) -> ((1st` o) = f -> f e. t)))
130	129	com12 14	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((1st` o) = f -> f e. t)))
131		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . 24 |- <.d, t>. e. _V
132		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = <.d, t>. -> (x = <.u, h>. <-> <.d, t>. = <.u, h>.))
133	132	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = <.d, t>. -> ((x = <.u, h>. /\ y = <.v, g>.) <-> (<.d, t>. = <.u, h>. /\ y = <.v, g>.)))
134	133	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x = <.d, t>. -> (((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
135	134	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (x = <.d, t>. -> (E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
136	135	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x = <.d, t>. -> (E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
137		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = o -> (y = <.v, g>. <-> o = <.v, g>.))
138	137	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (y = o -> ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) <-> (<.d, t>. = <.u, h>. /\ o = <.v, g>.)))
139	138	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y = o -> (((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
140	139	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y = o -> (E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
141	140	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = o -> (E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
142		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . 24 |- {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}
143	131, 104, 136, 141, 142	brab 3571	. . . . . . . . . . . . . . . . . . . . . . 23 |- (<.d, t>.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}o <-> E.u e. X E.v e. X E.h e. F E.g e. F ((<.d, t>. = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)))
144	130, 143	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (<.d, t>.{<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}o -> ((1st` o) = f -> f e. t)))
145	107, 144	sylbid 220	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) -> ((1st` o) = f -> f e. t)))
146	145	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (E.o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)(1st` o) = f -> f e. t))
147		fvelima 4723	. . . . . . . . . . . . . . . . . . . . 21 |- ((Fun 1st /\ f e. (1st"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.))) -> E.o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)(1st` o) = f)
148	5, 147	mpan 759	. . . . . . . . . . . . . . . . . . . 20 |- (f e. (1st"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) -> E.o e. ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)(1st` o) = f)
149	146, 148	syl5 20	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (f e. (1st"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) -> f e. t))
150	149	ssrdv 2622	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> (1st"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t)
151		df-ima 4007	. . . . . . . . . . . . . . . . . 18 |- (1st"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) = ran (1st |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.))
152	150, 151	syl5ssr 2662	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ran (1st |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t)
153	102, 152	eqsstrd 2651	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ran ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t)
154		df-ima 4007	. . . . . . . . . . . . . . . 16 |- ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) = ran ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) |` ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.))
155	153, 154	syl5ss 2661	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t)
156		imaeq2 4260	. . . . . . . . . . . . . . . . 17 |- (z = ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) = ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)))
157	156	sseq1d 2644	. . . . . . . . . . . . . . . 16 |- (z = ((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) -> (((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t <-> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t))
158	157	rcla4ev 2381	. . . . . . . . . . . . . . 15 |- ((((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.) e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) /\ ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"((tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})` <.d, t>.)) C_ t) -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)
159	92, 155, 158	syl11anc 524	. . . . . . . . . . . . . 14 |- ((F e. Fil /\ (t e. F /\ d e. t)) -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)
160	159	expr 418	. . . . . . . . . . . . 13 |- ((F e. Fil /\ t e. F) -> (d e. t -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t))
161	160	19.23adv 1584	. . . . . . . . . . . 12 |- ((F e. Fil /\ t e. F) -> (E.d d e. t -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t))
162	161	ex 402	. . . . . . . . . . 11 |- (F e. Fil -> (t e. F -> (E.d d e. t -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
163	68, 162	mpdd 57	. . . . . . . . . 10 |- (F e. Fil -> (t e. F -> E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t))
164	61, 163	jcad 661	. . . . . . . . 9 |- (F e. Fil -> (t e. F -> (t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
165	1	filnetlem5 15644	. . . . . . . . 9 |- (F e. Fil -> ((t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t) -> t e. F))
166	164, 165	impbid 574	. . . . . . . 8 |- (F e. Fil -> (t e. F <-> (t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
167	166	adantr 425	. . . . . . 7 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> (t e. F <-> (t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
168	8	adantr 425	. . . . . . . 8 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> X e. _V)
169	2	adantr 425	. . . . . . . . 9 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir)
170	1	filusb 10267	. . . . . . . . . . . . . 14 |- (F e. Fil -> X e. F)
171		eleq1 1957	. . . . . . . . . . . . . . 15 |- (r = X -> (r e. F <-> X e. F))
172	171	cla4egv 2365	. . . . . . . . . . . . . 14 |- (X e. _V -> (X e. F -> E.r r e. F))
173	8, 170, 172	sylc 83	. . . . . . . . . . . . 13 |- (F e. Fil -> E.r r e. F)
174		eleq1 1957	. . . . . . . . . . . . . . . . . . 19 |- (r = (/) -> (r e. F <-> (/) e. F))
175	174	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (r = (/) -> (-. r e. F <-> -. (/) e. F))
176	175, 64	syl5cbir 228	. . . . . . . . . . . . . . . . 17 |- (F e. Fil -> (r = (/) -> -. r e. F))
177	176	necon2ad 2055	. . . . . . . . . . . . . . . 16 |- (F e. Fil -> (r e. F -> r =/= (/)))
178		n0 2884	. . . . . . . . . . . . . . . 16 |- (r =/= (/) <-> E.s s e. r)
179	177, 178	syl6ib 229	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (r e. F -> E.s s e. r))
180		simpr 350	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ r e. F) -> r e. F)
181	180	a1d 15	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ r e. F) -> (s e. r -> r e. F))
182	181	ancrd 323	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ r e. F) -> (s e. r -> (r e. F /\ s e. r)))
183	182	eximdv 1669	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ r e. F) -> (E.s s e. r -> E.s(r e. F /\ s e. r)))
184	183	ex 402	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (r e. F -> (E.s s e. r -> E.s(r e. F /\ s e. r))))
185	179, 184	mpdd 57	. . . . . . . . . . . . . 14 |- (F e. Fil -> (r e. F -> E.s(r e. F /\ s e. r)))
186	185	eximdv 1669	. . . . . . . . . . . . 13 |- (F e. Fil -> (E.r r e. F -> E.rE.s(r e. F /\ s e. r)))
187	173, 186	mpd 29	. . . . . . . . . . . 12 |- (F e. Fil -> E.rE.s(r e. F /\ s e. r))
188		visset 2295	. . . . . . . . . . . . . . 15 |- s e. _V
189		visset 2295	. . . . . . . . . . . . . . 15 |- r e. _V
190		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (m = s -> (m e. n <-> s e. n))
191	190	anbi2d 678	. . . . . . . . . . . . . . 15 |- (m = s -> ((n e. F /\ m e. n) <-> (n e. F /\ s e. n)))
192		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (n = r -> (n e. F <-> r e. F))
193		eleq2 1958	. . . . . . . . . . . . . . . 16 |- (n = r -> (s e. n <-> s e. r))
194	192, 193	anbi12d 690	. . . . . . . . . . . . . . 15 |- (n = r -> ((n e. F /\ s e. n) <-> (r e. F /\ s e. r)))
195	188, 189, 191, 194	opelopab 3570	. . . . . . . . . . . . . 14 |- (<.s, r>. e. {<.m, n>. | (n e. F /\ m e. n)} <-> (r e. F /\ s e. r))
196		ne0i 2881	. . . . . . . . . . . . . 14 |- (<.s, r>. e. {<.m, n>. | (n e. F /\ m e. n)} -> {<.m, n>. | (n e. F /\ m e. n)} =/= (/))
197	195, 196	sylbir 218	. . . . . . . . . . . . 13 |- ((r e. F /\ s e. r) -> {<.m, n>. | (n e. F /\ m e. n)} =/= (/))
198	197	19.23aivv 1675	. . . . . . . . . . . 12 |- (E.rE.s(r e. F /\ s e. r) -> {<.m, n>. | (n e. F /\ m e. n)} =/= (/))
199	187, 198	syl 12	. . . . . . . . . . 11 |- (F e. Fil -> {<.m, n>. | (n e. F /\ m e. n)} =/= (/))
200	85, 86	syl6req 1945	. . . . . . . . . . . 12 |- (F e. Fil -> {<.m, n>. | (n e. F /\ m e. n)} = dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
201	200	neeq1d 2028	. . . . . . . . . . 11 |- (F e. Fil -> ({<.m, n>. | (n e. F /\ m e. n)} =/= (/) <-> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} =/= (/)))
202	199, 201	mpbid 212	. . . . . . . . . 10 |- (F e. Fil -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} =/= (/))
203	202	adantr 425	. . . . . . . . 9 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} =/= (/))
204	69	tailfb 15639	. . . . . . . . 9 |- (({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir /\ dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} =/= (/)) -> ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. fBas)
205	169, 203, 204	syl11anc 524	. . . . . . . 8 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. fBas)
206	69	tailuni 15638	. . . . . . . . . . . 12 |- ({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir -> U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) = dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
207	2, 206	syl 12	. . . . . . . . . . 11 |- (F e. Fil -> U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) = dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
208	207	eqcomd 1889	. . . . . . . . . 10 |- (F e. Fil -> dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} = U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))
209	208	feq2d 4557	. . . . . . . . 9 |- (F e. Fil -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X <-> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})-->X))
210	209	biimpa 460	. . . . . . . 8 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})-->X)
211		eqid 1884	. . . . . . . . 9 |- U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) = U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
212	211	elfilmap 10312	. . . . . . . 8 |- ((X e. _V /\ ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. fBas /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):U.ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})-->X) -> (t e. ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})) <-> (t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
213	168, 205, 210, 212	syl111anc 1100	. . . . . . 7 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> (t e. ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})) <-> (t C_ X /\ E.z e. ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})"z) C_ t)))
214	167, 213	bitr4d 590	. . . . . 6 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> (t e. F <-> t e. ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))))
215	214	eqrdv 1882	. . . . 5 |- ((F e. Fil /\ (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X) -> F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})))
216	215	ex 402	. . . 4 |- (F e. Fil -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X -> F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))))
217	58, 216	jcai 313	. . 3 |- (F e. Fil -> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))))
218		feq1 4551	. . . . 5 |- (f = (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> (f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X <-> (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X))
219		fveq2 4681	. . . . . 6 |- (f = (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f) = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})))
220	219	eqeq2d 1895	. . . . 5 |- (f = (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> (F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f) <-> F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))))
221	218, 220	anbi12d 690	. . . 4 |- (f = (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) -> ((f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f)) <-> ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})))))
222	221	cla4egv 2365	. . 3 |- ((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}) e. _V -> (((1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}):dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` (1st |` dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))) -> E.f(f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f))))
223	34, 217, 222	sylc 83	. 2 |- (F e. Fil -> E.f(f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f)))
224		dmeq 4157	. . . . . 6 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> dom d = dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})
225	224	feq2d 4557	. . . . 5 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (f:dom d-->X <-> f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X))
226		fveq2 4681	. . . . . . . . 9 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (tail` d) = (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))
227	226	rneqd 4188	. . . . . . . 8 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> ran (tail` d) = ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))
228	227	opreq2d 4898	. . . . . . 7 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (X FilMap ran (tail` d)) = (X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))})))
229	228	fveq1d 4683	. . . . . 6 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> ((X FilMap ran (tail` d))` f) = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f))
230	229	eqeq2d 1895	. . . . 5 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (F = ((X FilMap ran (tail` d))` f) <-> F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f)))
231	225, 230	anbi12d 690	. . . 4 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> ((f:dom d-->X /\ F = ((X FilMap ran (tail` d))` f)) <-> (f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f))))
232	231	exbidv 1657	. . 3 |- (d = {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} -> (E.f(f:dom d-->X /\ F = ((X FilMap ran (tail` d))` f)) <-> E.f(f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f))))
233	232	rcla4ev 2381	. 2 |- (({<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))} e. Dir /\ E.f(f:dom {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}-->X /\ F = ((X FilMap ran (tail` {<.x, y>. | E.u e. X E.v e. X E.h e. F E.g e. F ((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))}))` f))) -> E.d e. Dir E.f(f:dom d-->X /\ F = ((X FilMap ran (tail` d))` f)))
234	2, 223, 233	syl11anc 524	1 |- (F e. Fil -> E.d e. Dir E.f(f:dom d-->X /\ F = ((X FilMap ran (tail` d))` f)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  E.wrex 2106  _Vcvv 2292   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  <.cop 3046  U.cuni 3177   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  1stc1st 5018  fBascfbas 10257  Filcfil 10264   FilMap cfilmap 10304  Dircdir 10348  tailctail 10349

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-nel 2020  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  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-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-map 5383  df-fbas 10259  df-fg 10260  df-fil 10265  df-filmap 10306  df-dir 10350  df-tail 10351

Copyright terms: Public domain