Theorem filnetlem5 15644

Description: Lemma for filnet 15645.

Hypothesis

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

Assertion

Ref	Expression
filnetlem5	|- (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))

Distinct variable groups:   g,h,t,u,v,x,y,z,F   g,X,h,t,u,v,x,y,z

Proof of Theorem filnetlem5

Step	Hyp	Ref	Expression
1		simpll 448	. . . . . 6 |- (((F e. Fil /\ 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 C_ X)) -> F e. Fil)
2		filnet.1	. . . . . . . . . . . . 13 |- X = U.F
3	2	filnetlem4 15643	. . . . . . . . . . . 12 |- (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)
4		eqid 1884	. . . . . . . . . . . . 13 |- 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))}
5	4	tailmap 15636	. . . . . . . . . . . 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 -> (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))})
6		ffn 4562	. . . . . . . . . . . 12 |- ((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))})
7	3, 5, 6	3syl 24	. . . . . . . . . . 11 |- (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))})
8		fvelrnb 4719	. . . . . . . . . . 11 |- ((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))} -> (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))}) <-> E.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))})` t) = z))
9	7, 8	syl 12	. . . . . . . . . 10 |- (F e. Fil -> (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))}) <-> E.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))})` t) = z))
10		imaeq2 4260	. . . . . . . . . . . . 13 |- (((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))})` t) = 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))})` 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))
11	10	eleq1d 1963	. . . . . . . . . . . 12 |- (((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))})` t) = 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))})` t)) e. 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))})"z) e. F))
12		dirdm 10354	. . . . . . . . . . . . . . . . 17 |- ({<.x, y>. | E.u e. X E.v e. 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))})
13	3, 12	syl 12	. . . . . . . . . . . . . . . 16 |- (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))})
14	2	filnetlem1 15640	. . . . . . . . . . . . . . . 16 |- 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)}
15	13, 14	syl6eq 1944	. . . . . . . . . . . . . . 15 |- (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)})
16	15	eleq2d 1964	. . . . . . . . . . . . . 14 |- (F e. Fil -> (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))} <-> t e. {<.m, n>. | (n e. F /\ m e. n)}))
17	3, 5	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (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))})
18	17	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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))})
19	13, 14	syl6req 1945	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (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))})
20	19	eleq2d 1964	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> (t e. {<.m, n>. | (n e. F /\ m e. n)} <-> 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))}))
21		19.8a 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> E.n(t = <.m, n>. /\ (n e. F /\ m e. n)))
22		19.8a 1376	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.n(t = <.m, n>. /\ (n e. F /\ m e. n)) -> E.mE.n(t = <.m, n>. /\ (n e. F /\ m e. n)))
23		elopab 3559	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (t e. {<.m, n>. | (n e. F /\ m e. n)} <-> E.mE.n(t = <.m, n>. /\ (n e. F /\ m e. n)))
24	23	biimpri 169	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (E.mE.n(t = <.m, n>. /\ (n e. F /\ m e. n)) -> t e. {<.m, n>. | (n e. F /\ m e. n)})
25	21, 22, 24	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> t e. {<.m, n>. | (n e. F /\ m e. n)})
26	20, 25	syl5bi 225	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F e. Fil -> ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> 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))}))
27	26	imp 377	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> 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))})
28		ffvelrn 4787	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((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))} /\ 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))})` 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))})
29	18, 27, 28	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((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))})` 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))})
30		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((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))})` t) e. _V
31	30	elpw 3037	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((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))})` 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))})` 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))})
32	29, 31	sylib 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((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))})` 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))})
33		resabs1 4244	. . . . . . . . . . . . . . . . . . . . . 22 |- (((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))})` 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))})` 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))})` t)))
34	32, 33	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((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))})` 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))})` t)))
35	34	rneqd 4188	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> 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))})` 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))})` t)))
36	3	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> {<.x, y>. | E.u e. X E.v e. 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)
37		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- o e. _V
38	4	eltail 15635	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (({<.x, y>. | E.u e. X E.v e. 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 /\ 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))})` t) <-> 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))
39	37, 38	mp3an3 1180	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (({<.x, y>. | E.u e. X E.v e. 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 /\ 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))})` t) <-> 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))
40	36, 27, 39	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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))})` t) <-> 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))
41		simpr3 884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> g C_ h)
42	41	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> g C_ h)
43		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ((t = <.u, h>. /\ t = <.m, n>.) -> <.u, h>. = <.m, n>.)
44		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- h e. _V
45		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 |- n e. _V
46	44, 45	opth2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- (<.u, h>. = <.m, n>. -> h = n)
47	43, 46	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ((t = <.u, h>. /\ t = <.m, n>.) -> h = n)
48	47	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- (((t = <.u, h>. /\ o = <.v, g>.) /\ t = <.m, n>.) -> h = n)
49	48	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ t = <.m, n>.)) -> h = n)
50	49	adantrrr 439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n)))) -> h = n)
51	50	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> h = n)
52	42, 51	sseqtrd 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> g C_ n)
53	52	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> g C_ n)
54		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> (1st` o) = d)
55		simplr 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> o = <.v, g>.)
56	55	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> o = <.v, g>.)
57	56	fveq2d 4685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> (1st` o) = (1st` <.v, g>.))
58		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- v e. _V
59	58	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- (1st` <.v, g>.) = v
60	57, 59	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) -> (1st` o) = v)
61	60	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> (1st` o) = v)
62	54, 61	eqtr3d 1927	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> d = v)
63		simplr2 919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n)))) -> v e. g)
64	63	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> v e. g)
65	62, 64	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> d e. g)
66	53, 65	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((((u e. X /\ v e. X) /\ (h e. F /\ g e. F)) /\ (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) /\ (F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))))) /\ (1st` o) = d) -> d e. n)
67	66	exp53 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((u e. X /\ v e. X) -> ((h e. F /\ g e. F) -> (((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((1st` o) = d -> d e. n)))))
68	67	r19.23advv 2218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((u e. X /\ v e. X) -> (E.h e. F E.g e. F ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((1st` o) = d -> d e. n))))
69	68	r19.23aivv 2217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (E.u e. X E.v e. X E.h e. F E.g e. F ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((1st` o) = d -> d e. n)))
70	69	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (E.u e. X E.v e. X E.h e. F E.g e. F ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) -> ((1st` o) = d -> d e. n)))
71		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- t e. _V
72		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (x = t -> (x = <.u, h>. <-> t = <.u, h>.))
73	72	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (x = t -> ((x = <.u, h>. /\ y = <.v, g>.) <-> (t = <.u, h>. /\ y = <.v, g>.)))
74	73	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = t -> (((x = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
75	74	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = 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 ((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
76	75	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = 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 ((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
77		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = o -> (y = <.v, g>. <-> o = <.v, g>.))
78	77	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = o -> ((t = <.u, h>. /\ y = <.v, g>.) <-> (t = <.u, h>. /\ o = <.v, g>.)))
79	78	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = o -> (((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
80	79	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y = o -> (E.h e. F E.g e. F ((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
81	80	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y = o -> (E.u e. X E.v e. X E.h e. F E.g e. F ((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 ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
82		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {<.x, y>. | E.u e. X E.v e. 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))}
83	71, 37, 76, 81, 82	brab 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (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 ((t = <.u, h>. /\ o = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)))
84	70, 83	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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) = d -> d e. n)))
85	40, 84	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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))})` t) -> ((1st` o) = d -> d e. n)))
86	85	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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))})` t)(1st` o) = d -> d e. n))
87		fo1st 5032	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- 1st:_V-onto->_V
88		fofun 4618	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1st:_V-onto->_V -> Fun 1st)
89	87, 88	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- Fun 1st
90		fvelima 4723	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((Fun 1st /\ d 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))})` 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))})` t)(1st` o) = d)
91	89, 90	mpan 759	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d 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))})` 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))})` t)(1st` o) = d)
92	86, 91	syl5 20	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d 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))})` t)) -> d e. n))
93		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((m e. n /\ n e. F) -> m e. U.F)
94	93	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((n e. F /\ m e. n) -> m e. U.F)
95	94, 2	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((n e. F /\ m e. n) -> m e. X)
96	95	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> m e. X)
97	96	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> m e. X)
98		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ((d e. n /\ n e. F) -> d e. U.F)
99	98	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ((n e. F /\ d e. n) -> d e. U.F)
100	99, 2	syl6eleqr 1982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((n e. F /\ d e. n) -> d e. X)
101	100	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((n e. F /\ m e. n) /\ d e. n) -> d e. X)
102	101	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((t = <.m, n>. /\ (n e. F /\ m e. n)) /\ d e. n) -> d e. X)
103	102	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> d e. X)
104		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> n e. F)
105	104	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> n e. F)
106		simplrl 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> t = <.m, n>.)
107		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- <.d, n>. = <.d, n>.
108	106, 107	jctir 317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> (t = <.m, n>. /\ <.d, n>. = <.d, n>.))
109		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> m e. n)
110	109	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> m e. n)
111		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> d e. n)
112		ssid 2634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- n C_ n
113	112	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> n C_ n)
114	110, 111, 113	3jca 1050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> (m e. n /\ d e. n /\ n C_ n))
115		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (h = n -> <.m, h>. = <.m, n>.)
116	115	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h = n -> (t = <.m, h>. <-> t = <.m, n>.))
117	116	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (h = n -> ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) <-> (t = <.m, n>. /\ <.d, n>. = <.d, g>.)))
118		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h = n -> (m e. h <-> m e. n))
119		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (h = n -> (g C_ h <-> g C_ n))
120	118, 119	3anbi13d 1170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (h = n -> ((m e. h /\ d e. g /\ g C_ h) <-> (m e. n /\ d e. g /\ g C_ n)))
121	117, 120	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (h = n -> (((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h)) <-> ((t = <.m, n>. /\ <.d, n>. = <.d, g>.) /\ (m e. n /\ d e. g /\ g C_ n))))
122		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (g = n -> <.d, g>. = <.d, n>.)
123	122	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (g = n -> (<.d, n>. = <.d, g>. <-> <.d, n>. = <.d, n>.))
124	123	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (g = n -> ((t = <.m, n>. /\ <.d, n>. = <.d, g>.) <-> (t = <.m, n>. /\ <.d, n>. = <.d, n>.)))
125		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (g = n -> (d e. g <-> d e. n))
126		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (g = n -> (g C_ n <-> n C_ n))
127	125, 126	3anbi23d 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (g = n -> ((m e. n /\ d e. g /\ g C_ n) <-> (m e. n /\ d e. n /\ n C_ n)))
128	124, 127	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (g = n -> (((t = <.m, n>. /\ <.d, n>. = <.d, g>.) /\ (m e. n /\ d e. g /\ g C_ n)) <-> ((t = <.m, n>. /\ <.d, n>. = <.d, n>.) /\ (m e. n /\ d e. n /\ n C_ n))))
129	121, 128	rcla42ev 2385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((n e. F /\ n e. F /\ ((t = <.m, n>. /\ <.d, n>. = <.d, n>.) /\ (m e. n /\ d e. n /\ n C_ n))) -> E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h)))
130	105, 105, 108, 114, 129	syl112anc 1104	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h)))
131		opeq1 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (u = m -> <.u, h>. = <.m, h>.)
132	131	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u = m -> (t = <.u, h>. <-> t = <.m, h>.))
133	132	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u = m -> ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) <-> (t = <.m, h>. /\ <.d, n>. = <.v, g>.)))
134		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (u = m -> (u e. h <-> m e. h))
135	134	3anbi1d 1172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (u = m -> ((u e. h /\ v e. g /\ g C_ h) <-> (m e. h /\ v e. g /\ g C_ h)))
136	133, 135	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (u = m -> (((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((t = <.m, h>. /\ <.d, n>. = <.v, g>.) /\ (m e. h /\ v e. g /\ g C_ h))))
137	136	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (u = m -> (E.h e. F E.g e. F ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.v, g>.) /\ (m e. h /\ v e. g /\ g C_ h))))
138		opeq1 3158	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- (v = d -> <.v, g>. = <.d, g>.)
139	138	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = d -> (<.d, n>. = <.v, g>. <-> <.d, n>. = <.d, g>.))
140	139	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = d -> ((t = <.m, h>. /\ <.d, n>. = <.v, g>.) <-> (t = <.m, h>. /\ <.d, n>. = <.d, g>.)))
141		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (v = d -> (v e. g <-> d e. g))
142	141	3anbi2d 1173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (v = d -> ((m e. h /\ v e. g /\ g C_ h) <-> (m e. h /\ d e. g /\ g C_ h)))
143	140, 142	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (v = d -> (((t = <.m, h>. /\ <.d, n>. = <.v, g>.) /\ (m e. h /\ v e. g /\ g C_ h)) <-> ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h))))
144	143	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (v = d -> (E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.v, g>.) /\ (m e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h))))
145	137, 144	rcla42ev 2385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((m e. X /\ d e. X /\ E.h e. F E.g e. F ((t = <.m, h>. /\ <.d, n>. = <.d, g>.) /\ (m e. h /\ d e. g /\ g C_ h))) -> E.u e. X E.v e. X E.h e. F E.g e. F ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)))
146	97, 103, 130, 145	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> E.u e. X E.v e. X E.h e. F E.g e. F ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)))
147		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- <.d, n>. e. _V
148		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- (y = <.d, n>. -> (y = <.v, g>. <-> <.d, n>. = <.v, g>.))
149	148	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- (y = <.d, n>. -> ((t = <.u, h>. /\ y = <.v, g>.) <-> (t = <.u, h>. /\ <.d, n>. = <.v, g>.)))
150	149	anbi1d 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (y = <.d, n>. -> (((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
151	150	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (y = <.d, n>. -> (E.h e. F E.g e. F ((t = <.u, h>. /\ y = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)) <-> E.h e. F E.g e. F ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
152	151	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (y = <.d, n>. -> (E.u e. X E.v e. X E.h e. F E.g e. F ((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 ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h))))
153	71, 147, 76, 152, 82	brab 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (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))}<.d, n>. <-> E.u e. X E.v e. X E.h e. F E.g e. F ((t = <.u, h>. /\ <.d, n>. = <.v, g>.) /\ (u e. h /\ v e. g /\ g C_ h)))
154	146, 153	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> 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))}<.d, n>.)
155	3	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> {<.x, y>. | E.u e. X E.v e. 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)
156	25	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> t e. {<.m, n>. | (n e. F /\ m e. n)})
157	16	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> (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))} <-> t e. {<.m, n>. | (n e. F /\ m e. n)}))
158	156, 157	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> 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))})
159	147	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> <.d, n>. e. _V)
160	4	eltail 15635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (({<.x, y>. | E.u e. X E.v e. 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 /\ 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, n>. e. _V) -> (<.d, n>. 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))})` t) <-> 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))}<.d, n>.))
161	155, 158, 159, 160	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> (<.d, n>. 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))})` t) <-> 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))}<.d, n>.))
162	154, 161	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) /\ d e. n) -> <.d, n>. 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))})` t))
163	162	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d e. n -> <.d, n>. 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))})` t)))
164		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- d e. _V
165	164	op1st 5026	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (1st` <.d, n>.) = d
166	165	a1i12 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d e. n -> (1st` <.d, n>.) = d))
167	163, 166	jcad 661	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d e. n -> (<.d, n>. 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))})` t) /\ (1st` <.d, n>.) = d)))
168		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (f = <.d, n>. -> (1st` f) = (1st` <.d, n>.))
169	168	eqeq1d 1892	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (f = <.d, n>. -> ((1st` f) = d <-> (1st` <.d, n>.) = d))
170	169	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((<.d, n>. 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))})` t) /\ (1st` <.d, n>.) = d) -> E.f 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))})` t)(1st` f) = d)
171	167, 170	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d e. n -> E.f 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))})` t)(1st` f) = d))
172		fofn 4619	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (1st:_V-onto->_V -> 1st Fn _V)
173	87, 172	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- 1st Fn _V
174		ssv 2636	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((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))})` t) C_ _V
175		fvelimab 4725	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((1st Fn _V /\ ((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))})` t) C_ _V) -> (d 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))})` t)) <-> E.f 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))})` t)(1st` f) = d))
176	173, 174, 175	mp2an 761	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (d 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))})` t)) <-> E.f 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))})` t)(1st` f) = d)
177	171, 176	syl6ibr 230	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d e. n -> d 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))})` t))))
178	92, 177	impbid 574	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (d 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))})` t)) <-> d e. n))
179	178	eqrdv 1882	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> (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))})` t)) = n)
180		df-ima 4007	. . . . . . . . . . . . . . . . . . . . 21 |- (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))})` 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))})` t))
181	179, 180	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> 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))})` t)) = n)
182	35, 181	eqtrd 1925	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> 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))})` t)) = n)
183		df-ima 4007	. . . . . . . . . . . . . . . . . . 19 |- ((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))})` 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))})` t))
184	182, 183	syl5eq 1940	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((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))})` t)) = n)
185		simprrl 458	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> n e. F)
186	184, 185	eqeltrd 1971	. . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (t = <.m, n>. /\ (n e. F /\ m e. n))) -> ((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))})` t)) e. F)
187	186	ex 402	. . . . . . . . . . . . . . . 16 |- (F e. Fil -> ((t = <.m, n>. /\ (n e. F /\ m e. n)) -> ((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))})` t)) e. F))
188	187	19.23advv 1676	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (E.mE.n(t = <.m, n>. /\ (n e. F /\ m e. n)) -> ((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))})` t)) e. F))
189	188, 23	syl5ib 223	. . . . . . . . . . . . . 14 |- (F e. Fil -> (t e. {<.m, n>. | (n e. F /\ m e. n)} -> ((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))})` t)) e. F))
190	16, 189	sylbid 220	. . . . . . . . . . . . 13 |- (F e. Fil -> (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))} -> ((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))})` t)) e. F))
191	190	imp 377	. . . . . . . . . . . 12 |- ((F e. Fil /\ 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))}) -> ((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))})` t)) e. F)
192	11, 191	syl5cbi 226	. . . . . . . . . . 11 |- ((F e. Fil /\ 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))})` t) = 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))})"z) e. F))
193	192	r19.23adva 2216	. . . . . . . . . 10 |- (F e. Fil -> (E.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))})` t) = 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))})"z) e. F))
194	9, 193	sylbid 220	. . . . . . . . 9 |- (F e. Fil -> (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) e. F))
195	194	imp 377	. . . . . . . 8 |- ((F e. Fil /\ 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) e. F)
196	195	adantr 425	. . . . . . 7 |- (((F e. Fil /\ 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 C_ 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))})"z) e. F)
197		simprr 451	. . . . . . 7 |- (((F e. Fil /\ 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 C_ X)) -> t C_ X)
198		simprl 450	. . . . . . 7 |- (((F e. Fil /\ 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 C_ 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))})"z) C_ t)
199	196, 197, 198	3jca 1050	. . . . . 6 |- (((F e. Fil /\ 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 C_ 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))})"z) e. F /\ t C_ 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))})"z) C_ t))
200	2	fillsb 10270	. . . . . 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))})"z) e. F /\ t C_ 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))})"z) C_ t) -> t e. F))
201	1, 199, 200	sylc 83	. . . . 5 |- (((F e. Fil /\ 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 C_ X)) -> t e. F)
202	201	exp43 415	. . . 4 |- (F e. Fil -> (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 C_ X -> t e. F))))
203	202	r19.23adv 2215	. . 3 |- (F e. Fil -> (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 C_ X -> t e. F)))
204	203	com23 36	. 2 |- (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)))
205	204	imp3a 388	1 |- (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))

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

This theorem is referenced by:  filnet 15645

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-v 2294  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-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-1st 5020  df-fil 10265  df-dir 10350  df-tail 10351

Copyright terms: Public domain