filnetlem4

	Ref	Expression
Hypotheses	filnet.h	$⊢ H = ⋃_{n \in F} (\{n\} \times n)$
	filnet.d	$⊢ D = \{⟨x, y⟩ \| ((x \in H \land y \in H) \land 1^{st} (y) \subseteq 1^{st} (x))\}$
Assertion	filnetlem4	$⊢ F \in Fil (X) \to \exists d \in DirRel \exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d)))$

Proof

Step	Hyp	Ref	Expression
1		filnet.h	$⊢ H = ⋃_{n \in F} (\{n\} \times n)$
2		filnet.d	$⊢ D = \{⟨x, y⟩ \| ((x \in H \land y \in H) \land 1^{st} (y) \subseteq 1^{st} (x))\}$
3	1 2	filnetlem3	$⊢ (H = ⋃ ⋃ D \land (F \in Fil (X) \to (H \subseteq F \times X \land D \in DirRel)))$
4	3	simpri	$⊢ F \in Fil (X) \to (H \subseteq F \times X \land D \in DirRel)$
5	4	simprd	$⊢ F \in Fil (X) \to D \in DirRel$
6		f2ndres	$⊢ ({2^{nd} ↾}_{(F \times X)}) : F \times X ⟶ X$
7	4	simpld	$⊢ F \in Fil (X) \to H \subseteq F \times X$
8		fssres2	$⊢ (({2^{nd} ↾}_{(F \times X)}) : F \times X ⟶ X \land H \subseteq F \times X) \to ({2^{nd} ↾}_{H}) : H ⟶ X$
9	6 7 8	sylancr	$⊢ F \in Fil (X) \to ({2^{nd} ↾}_{H}) : H ⟶ X$
10		filtop	$⊢ F \in Fil (X) \to X \in F$
11		xpexg	$⊢ (F \in Fil (X) \land X \in F) \to F \times X \in V$
12	10 11	mpdan	$⊢ F \in Fil (X) \to F \times X \in V$
13	12 7	ssexd	$⊢ F \in Fil (X) \to H \in V$
14	9 13	fexd	$⊢ F \in Fil (X) \to {2^{nd} ↾}_{H} \in V$
15	3	simpli	$⊢ H = ⋃ ⋃ D$
16		dirdm	$⊢ D \in DirRel \to dom D = ⋃ ⋃ D$
17	5 16	syl	$⊢ F \in Fil (X) \to dom D = ⋃ ⋃ D$
18	15 17	eqtr4id	$⊢ F \in Fil (X) \to H = dom D$
19	18	feq2d	$⊢ F \in Fil (X) \to (({2^{nd} ↾}_{H}) : H ⟶ X \leftrightarrow ({2^{nd} ↾}_{H}) : dom D ⟶ X)$
20	9 19	mpbid	$⊢ F \in Fil (X) \to ({2^{nd} ↾}_{H}) : dom D ⟶ X$
21		eqid	$⊢ dom D = dom D$
22	21	tailf	$⊢ D \in DirRel \to tail (D) : dom D ⟶ 𝒫 dom D$
23	5 22	syl	$⊢ F \in Fil (X) \to tail (D) : dom D ⟶ 𝒫 dom D$
24	18	feq2d	$⊢ F \in Fil (X) \to (tail (D) : H ⟶ 𝒫 dom D \leftrightarrow tail (D) : dom D ⟶ 𝒫 dom D)$
25	23 24	mpbird	$⊢ F \in Fil (X) \to tail (D) : H ⟶ 𝒫 dom D$
26	25	adantr	$⊢ (F \in Fil (X) \land t \subseteq X) \to tail (D) : H ⟶ 𝒫 dom D$
27		ffn	$⊢ tail (D) : H ⟶ 𝒫 dom D \to tail (D) Fn H$
28		imaeq2	$⊢ d = tail (D) (f) \to ({2^{nd} ↾}_{H}) [d] = ({2^{nd} ↾}_{H}) [tail (D) (f)]$
29	28	sseq1d	$⊢ d = tail (D) (f) \to (({2^{nd} ↾}_{H}) [d] \subseteq t \leftrightarrow ({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t)$
30	29	rexrn	$⊢ tail (D) Fn H \to (\exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t \leftrightarrow \exists f \in H ({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t)$
31	26 27 30	3syl	$⊢ (F \in Fil (X) \land t \subseteq X) \to (\exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t \leftrightarrow \exists f \in H ({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t)$
32		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
33		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
34	32 33	ax-mp	$⊢ 2^{nd} Fn V$
35		ssv	$⊢ H \subseteq V$
36		fnssres	$⊢ (2^{nd} Fn V \land H \subseteq V) \to ({2^{nd} ↾}_{H}) Fn H$
37	34 35 36	mp2an	$⊢ ({2^{nd} ↾}_{H}) Fn H$
38		fnfun	$⊢ ({2^{nd} ↾}_{H}) Fn H \to Fun ({2^{nd} ↾}_{H})$
39	37 38	ax-mp	$⊢ Fun ({2^{nd} ↾}_{H})$
40	26	ffvelrnda	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to tail (D) (f) \in 𝒫 dom D$
41	40	elpwid	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to tail (D) (f) \subseteq dom D$
42	18	ad2antrr	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to H = dom D$
43	41 42	sseqtrrd	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to tail (D) (f) \subseteq H$
44	37	fndmi	$⊢ dom ({2^{nd} ↾}_{H}) = H$
45	43 44	sseqtrrdi	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to tail (D) (f) \subseteq dom ({2^{nd} ↾}_{H})$
46		funimass4	$⊢ (Fun ({2^{nd} ↾}_{H}) \land tail (D) (f) \subseteq dom ({2^{nd} ↾}_{H})) \to (({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t \leftrightarrow \forall d \in tail (D) (f) ({2^{nd} ↾}_{H}) (d) \in t)$
47	39 45 46	sylancr	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t \leftrightarrow \forall d \in tail (D) (f) ({2^{nd} ↾}_{H}) (d) \in t)$
48	5	ad2antrr	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to D \in DirRel$
49		simpr	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to f \in H$
50	49 42	eleqtrd	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to f \in dom D$
51		vex	$⊢ d \in V$
52	51	a1i	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to d \in V$
53	21	eltail	$⊢ (D \in DirRel \land f \in dom D \land d \in V) \to (d \in tail (D) (f) \leftrightarrow f D d)$
54	48 50 52 53	syl3anc	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (d \in tail (D) (f) \leftrightarrow f D d)$
55	49	biantrurd	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (d \in H \leftrightarrow (f \in H \land d \in H))$
56	55	anbi1d	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \leftrightarrow ((f \in H \land d \in H) \land 1^{st} (d) \subseteq 1^{st} (f)))$
57		vex	$⊢ f \in V$
58	1 2 57 51	filnetlem1	$⊢ f D d \leftrightarrow ((f \in H \land d \in H) \land 1^{st} (d) \subseteq 1^{st} (f))$
59	56 58	bitr4di	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \leftrightarrow f D d)$
60	54 59	bitr4d	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (d \in tail (D) (f) \leftrightarrow (d \in H \land 1^{st} (d) \subseteq 1^{st} (f)))$
61	60	imbi1d	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to ((d \in tail (D) (f) \to ({2^{nd} ↾}_{H}) (d) \in t) \leftrightarrow ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to ({2^{nd} ↾}_{H}) (d) \in t))$
62		fvres	$⊢ d \in H \to ({2^{nd} ↾}_{H}) (d) = 2^{nd} (d)$
63	62	eleq1d	$⊢ d \in H \to (({2^{nd} ↾}_{H}) (d) \in t \leftrightarrow 2^{nd} (d) \in t)$
64	63	adantr	$⊢ (d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to (({2^{nd} ↾}_{H}) (d) \in t \leftrightarrow 2^{nd} (d) \in t)$
65	64	pm5.74i	$⊢ ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to ({2^{nd} ↾}_{H}) (d) \in t) \leftrightarrow ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to 2^{nd} (d) \in t)$
66		impexp	$⊢ ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to 2^{nd} (d) \in t) \leftrightarrow (d \in H \to (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t))$
67	65 66	bitri	$⊢ ((d \in H \land 1^{st} (d) \subseteq 1^{st} (f)) \to ({2^{nd} ↾}_{H}) (d) \in t) \leftrightarrow (d \in H \to (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t))$
68	61 67	bitrdi	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to ((d \in tail (D) (f) \to ({2^{nd} ↾}_{H}) (d) \in t) \leftrightarrow (d \in H \to (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t)))$
69	68	ralbidv2	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (\forall d \in tail (D) (f) ({2^{nd} ↾}_{H}) (d) \in t \leftrightarrow \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t))$
70	47 69	bitrd	$⊢ ((F \in Fil (X) \land t \subseteq X) \land f \in H) \to (({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t \leftrightarrow \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t))$
71	70	rexbidva	$⊢ (F \in Fil (X) \land t \subseteq X) \to (\exists f \in H ({2^{nd} ↾}_{H}) [tail (D) (f)] \subseteq t \leftrightarrow \exists f \in H \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t))$
72		vex	$⊢ k \in V$
73		vex	$⊢ v \in V$
74	72 73	op1std	$⊢ d = ⟨k, v⟩ \to 1^{st} (d) = k$
75	74	sseq1d	$⊢ d = ⟨k, v⟩ \to (1^{st} (d) \subseteq 1^{st} (f) \leftrightarrow k \subseteq 1^{st} (f))$
76	72 73	op2ndd	$⊢ d = ⟨k, v⟩ \to 2^{nd} (d) = v$
77	76	eleq1d	$⊢ d = ⟨k, v⟩ \to (2^{nd} (d) \in t \leftrightarrow v \in t)$
78	75 77	imbi12d	$⊢ d = ⟨k, v⟩ \to ((1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow (k \subseteq 1^{st} (f) \to v \in t))$
79	78	raliunxp	$⊢ \forall d \in ⋃_{k \in F} (\{k\} \times k) (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \forall k \in F \forall v \in k (k \subseteq 1^{st} (f) \to v \in t)$
80		sneq	$⊢ n = k \to \{n\} = \{k\}$
81		id	$⊢ n = k \to n = k$
82	80 81	xpeq12d	$⊢ n = k \to \{n\} \times n = \{k\} \times k$
83	82	cbviunv	$⊢ ⋃_{n \in F} (\{n\} \times n) = ⋃_{k \in F} (\{k\} \times k)$
84	1 83	eqtri	$⊢ H = ⋃_{k \in F} (\{k\} \times k)$
85	84	raleqi	$⊢ \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \forall d \in ⋃_{k \in F} (\{k\} \times k) (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t)$
86		dfss3	$⊢ k \subseteq t \leftrightarrow \forall v \in k v \in t$
87	86	imbi2i	$⊢ (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow (k \subseteq 1^{st} (f) \to \forall v \in k v \in t)$
88		r19.21v	$⊢ \forall v \in k (k \subseteq 1^{st} (f) \to v \in t) \leftrightarrow (k \subseteq 1^{st} (f) \to \forall v \in k v \in t)$
89	87 88	bitr4i	$⊢ (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow \forall v \in k (k \subseteq 1^{st} (f) \to v \in t)$
90	89	ralbii	$⊢ \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow \forall k \in F \forall v \in k (k \subseteq 1^{st} (f) \to v \in t)$
91	79 85 90	3bitr4i	$⊢ \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t)$
92	91	rexbii	$⊢ \exists f \in H \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \exists f \in H \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t)$
93	1	rexeqi	$⊢ \exists f \in H \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow \exists f \in ⋃_{n \in F} (\{n\} \times n) \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t)$
94		vex	$⊢ n \in V$
95		vex	$⊢ m \in V$
96	94 95	op1std	$⊢ f = ⟨n, m⟩ \to 1^{st} (f) = n$
97	96	sseq2d	$⊢ f = ⟨n, m⟩ \to (k \subseteq 1^{st} (f) \leftrightarrow k \subseteq n)$
98	97	imbi1d	$⊢ f = ⟨n, m⟩ \to ((k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow (k \subseteq n \to k \subseteq t))$
99	98	ralbidv	$⊢ f = ⟨n, m⟩ \to (\forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow \forall k \in F (k \subseteq n \to k \subseteq t))$
100	99	rexiunxp	$⊢ \exists f \in ⋃_{n \in F} (\{n\} \times n) \forall k \in F (k \subseteq 1^{st} (f) \to k \subseteq t) \leftrightarrow \exists n \in F \exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t)$
101	92 93 100	3bitri	$⊢ \exists f \in H \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \exists n \in F \exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t)$
102		fileln0	$⊢ (F \in Fil (X) \land n \in F) \to n \neq \emptyset$
103	102	adantlr	$⊢ ((F \in Fil (X) \land t \subseteq X) \land n \in F) \to n \neq \emptyset$
104		r19.9rzv	$⊢ n \neq \emptyset \to (\forall k \in F (k \subseteq n \to k \subseteq t) \leftrightarrow \exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t))$
105	103 104	syl	$⊢ ((F \in Fil (X) \land t \subseteq X) \land n \in F) \to (\forall k \in F (k \subseteq n \to k \subseteq t) \leftrightarrow \exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t))$
106		ssid	$⊢ n \subseteq n$
107		sseq1	$⊢ k = n \to (k \subseteq n \leftrightarrow n \subseteq n)$
108		sseq1	$⊢ k = n \to (k \subseteq t \leftrightarrow n \subseteq t)$
109	107 108	imbi12d	$⊢ k = n \to ((k \subseteq n \to k \subseteq t) \leftrightarrow (n \subseteq n \to n \subseteq t))$
110	109	rspcv	$⊢ n \in F \to (\forall k \in F (k \subseteq n \to k \subseteq t) \to (n \subseteq n \to n \subseteq t))$
111	106 110	mpii	$⊢ n \in F \to (\forall k \in F (k \subseteq n \to k \subseteq t) \to n \subseteq t)$
112	111	adantl	$⊢ ((F \in Fil (X) \land t \subseteq X) \land n \in F) \to (\forall k \in F (k \subseteq n \to k \subseteq t) \to n \subseteq t)$
113		sstr2	$⊢ k \subseteq n \to (n \subseteq t \to k \subseteq t)$
114	113	com12	$⊢ n \subseteq t \to (k \subseteq n \to k \subseteq t)$
115	114	ralrimivw	$⊢ n \subseteq t \to \forall k \in F (k \subseteq n \to k \subseteq t)$
116	112 115	impbid1	$⊢ ((F \in Fil (X) \land t \subseteq X) \land n \in F) \to (\forall k \in F (k \subseteq n \to k \subseteq t) \leftrightarrow n \subseteq t)$
117	105 116	bitr3d	$⊢ ((F \in Fil (X) \land t \subseteq X) \land n \in F) \to (\exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t) \leftrightarrow n \subseteq t)$
118	117	rexbidva	$⊢ (F \in Fil (X) \land t \subseteq X) \to (\exists n \in F \exists m \in n \forall k \in F (k \subseteq n \to k \subseteq t) \leftrightarrow \exists n \in F n \subseteq t)$
119	101 118	syl5bb	$⊢ (F \in Fil (X) \land t \subseteq X) \to (\exists f \in H \forall d \in H (1^{st} (d) \subseteq 1^{st} (f) \to 2^{nd} (d) \in t) \leftrightarrow \exists n \in F n \subseteq t)$
120	31 71 119	3bitrd	$⊢ (F \in Fil (X) \land t \subseteq X) \to (\exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t \leftrightarrow \exists n \in F n \subseteq t)$
121	120	pm5.32da	$⊢ F \in Fil (X) \to ((t \subseteq X \land \exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t) \leftrightarrow (t \subseteq X \land \exists n \in F n \subseteq t))$
122		filn0	$⊢ F \in Fil (X) \to F \neq \emptyset$
123	94	snnz	$⊢ \{n\} \neq \emptyset$
124	102 123	jctil	$⊢ (F \in Fil (X) \land n \in F) \to (\{n\} \neq \emptyset \land n \neq \emptyset)$
125		neanior	$⊢ (\{n\} \neq \emptyset \land n \neq \emptyset) \leftrightarrow \neg (\{n\} = \emptyset \lor n = \emptyset)$
126	124 125	sylib	$⊢ (F \in Fil (X) \land n \in F) \to \neg (\{n\} = \emptyset \lor n = \emptyset)$
127		ss0b	$⊢ \{n\} \times n \subseteq \emptyset \leftrightarrow \{n\} \times n = \emptyset$
128		xpeq0	$⊢ \{n\} \times n = \emptyset \leftrightarrow (\{n\} = \emptyset \lor n = \emptyset)$
129	127 128	bitri	$⊢ \{n\} \times n \subseteq \emptyset \leftrightarrow (\{n\} = \emptyset \lor n = \emptyset)$
130	126 129	sylnibr	$⊢ (F \in Fil (X) \land n \in F) \to \neg \{n\} \times n \subseteq \emptyset$
131	130	ralrimiva	$⊢ F \in Fil (X) \to \forall n \in F \neg \{n\} \times n \subseteq \emptyset$
132		r19.2z	$⊢ (F \neq \emptyset \land \forall n \in F \neg \{n\} \times n \subseteq \emptyset) \to \exists n \in F \neg \{n\} \times n \subseteq \emptyset$
133	122 131 132	syl2anc	$⊢ F \in Fil (X) \to \exists n \in F \neg \{n\} \times n \subseteq \emptyset$
134		rexnal	$⊢ \exists n \in F \neg \{n\} \times n \subseteq \emptyset \leftrightarrow \neg \forall n \in F \{n\} \times n \subseteq \emptyset$
135	133 134	sylib	$⊢ F \in Fil (X) \to \neg \forall n \in F \{n\} \times n \subseteq \emptyset$
136	1	sseq1i	$⊢ H \subseteq \emptyset \leftrightarrow ⋃_{n \in F} (\{n\} \times n) \subseteq \emptyset$
137		ss0b	$⊢ H \subseteq \emptyset \leftrightarrow H = \emptyset$
138		iunss	$⊢ ⋃_{n \in F} (\{n\} \times n) \subseteq \emptyset \leftrightarrow \forall n \in F \{n\} \times n \subseteq \emptyset$
139	136 137 138	3bitr3i	$⊢ H = \emptyset \leftrightarrow \forall n \in F \{n\} \times n \subseteq \emptyset$
140	139	necon3abii	$⊢ H \neq \emptyset \leftrightarrow \neg \forall n \in F \{n\} \times n \subseteq \emptyset$
141	135 140	sylibr	$⊢ F \in Fil (X) \to H \neq \emptyset$
142		dmresi	$⊢ dom ({I ↾}_{H}) = H$
143	1 2	filnetlem2	$⊢ ({I ↾}_{H} \subseteq D \land D \subseteq H \times H)$
144	143	simpli	$⊢ {I ↾}_{H} \subseteq D$
145		dmss	$⊢ {I ↾}_{H} \subseteq D \to dom ({I ↾}_{H}) \subseteq dom D$
146	144 145	ax-mp	$⊢ dom ({I ↾}_{H}) \subseteq dom D$
147	142 146	eqsstrri	$⊢ H \subseteq dom D$
148	143	simpri	$⊢ D \subseteq H \times H$
149		dmss	$⊢ D \subseteq H \times H \to dom D \subseteq dom (H \times H)$
150	148 149	ax-mp	$⊢ dom D \subseteq dom (H \times H)$
151		dmxpid	$⊢ dom (H \times H) = H$
152	150 151	sseqtri	$⊢ dom D \subseteq H$
153	147 152	eqssi	$⊢ H = dom D$
154	153	tailfb	$⊢ (D \in DirRel \land H \neq \emptyset) \to ran tail (D) \in fBas (H)$
155	5 141 154	syl2anc	$⊢ F \in Fil (X) \to ran tail (D) \in fBas (H)$
156		elfm	$⊢ (X \in F \land ran tail (D) \in fBas (H) \land ({2^{nd} ↾}_{H}) : H ⟶ X) \to (t \in (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)) \leftrightarrow (t \subseteq X \land \exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t))$
157	10 155 9 156	syl3anc	$⊢ F \in Fil (X) \to (t \in (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)) \leftrightarrow (t \subseteq X \land \exists d \in ran tail (D) ({2^{nd} ↾}_{H}) [d] \subseteq t))$
158		filfbas	$⊢ F \in Fil (X) \to F \in fBas (X)$
159		elfg	$⊢ F \in fBas (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists n \in F n \subseteq t))$
160	158 159	syl	$⊢ F \in Fil (X) \to (t \in (X filGen F) \leftrightarrow (t \subseteq X \land \exists n \in F n \subseteq t))$
161	121 157 160	3bitr4d	$⊢ F \in Fil (X) \to (t \in (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)) \leftrightarrow t \in (X filGen F))$
162	161	eqrdv	$⊢ F \in Fil (X) \to (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)) = X filGen F$
163		fgfil	$⊢ F \in Fil (X) \to X filGen F = F$
164	162 163	eqtr2d	$⊢ F \in Fil (X) \to F = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D))$
165	20 164	jca	$⊢ F \in Fil (X) \to (({2^{nd} ↾}_{H}) : dom D ⟶ X \land F = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)))$
166		feq1	$⊢ f = {2^{nd} ↾}_{H} \to (f : dom D ⟶ X \leftrightarrow ({2^{nd} ↾}_{H}) : dom D ⟶ X)$
167		oveq2	$⊢ f = {2^{nd} ↾}_{H} \to X FilMap f = X FilMap ({2^{nd} ↾}_{H})$
168	167	fveq1d	$⊢ f = {2^{nd} ↾}_{H} \to (X FilMap f) (ran tail (D)) = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D))$
169	168	eqeq2d	$⊢ f = {2^{nd} ↾}_{H} \to (F = (X FilMap f) (ran tail (D)) \leftrightarrow F = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D)))$
170	166 169	anbi12d	$⊢ f = {2^{nd} ↾}_{H} \to ((f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D))) \leftrightarrow (({2^{nd} ↾}_{H}) : dom D ⟶ X \land F = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D))))$
171	170	spcegv	$⊢ {2^{nd} ↾}_{H} \in V \to ((({2^{nd} ↾}_{H}) : dom D ⟶ X \land F = (X FilMap ({2^{nd} ↾}_{H})) (ran tail (D))) \to \exists f (f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D))))$
172	14 165 171	sylc	$⊢ F \in Fil (X) \to \exists f (f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D)))$
173		dmeq	$⊢ d = D \to dom d = dom D$
174	173	feq2d	$⊢ d = D \to (f : dom d ⟶ X \leftrightarrow f : dom D ⟶ X)$
175		fveq2	$⊢ d = D \to tail (d) = tail (D)$
176	175	rneqd	$⊢ d = D \to ran tail (d) = ran tail (D)$
177	176	fveq2d	$⊢ d = D \to (X FilMap f) (ran tail (d)) = (X FilMap f) (ran tail (D))$
178	177	eqeq2d	$⊢ d = D \to (F = (X FilMap f) (ran tail (d)) \leftrightarrow F = (X FilMap f) (ran tail (D)))$
179	174 178	anbi12d	$⊢ d = D \to ((f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d))) \leftrightarrow (f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D))))$
180	179	exbidv	$⊢ d = D \to (\exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d))) \leftrightarrow \exists f (f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D))))$
181	180	rspcev	$⊢ (D \in DirRel \land \exists f (f : dom D ⟶ X \land F = (X FilMap f) (ran tail (D)))) \to \exists d \in DirRel \exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d)))$
182	5 172 181	syl2anc	$⊢ F \in Fil (X) \to \exists d \in DirRel \exists f (f : dom d ⟶ X \land F = (X FilMap f) (ran tail (d)))$

Metamath Proof Explorer

Theorem filnetlem4

Proof