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