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