filnetlem3

	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	filnetlem3	$⊢ (H = ⋃ ⋃ D \land (F \in Fil (X) \to (H \subseteq F \times X \land D \in DirRel)))$

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		dmresi	$⊢ dom ({I ↾}_{H}) = H$
4	1 2	filnetlem2	$⊢ ({I ↾}_{H} \subseteq D \land D \subseteq H \times H)$
5	4	simpli	$⊢ {I ↾}_{H} \subseteq D$
6		dmss	$⊢ {I ↾}_{H} \subseteq D \to dom ({I ↾}_{H}) \subseteq dom D$
7	5 6	ax-mp	$⊢ dom ({I ↾}_{H}) \subseteq dom D$
8	3 7	eqsstrri	$⊢ H \subseteq dom D$
9		ssun1	$⊢ dom D \subseteq dom D \cup ran D$
10	8 9	sstri	$⊢ H \subseteq dom D \cup ran D$
11		dmrnssfld	$⊢ dom D \cup ran D \subseteq ⋃ ⋃ D$
12	10 11	sstri	$⊢ H \subseteq ⋃ ⋃ D$
13	4	simpri	$⊢ D \subseteq H \times H$
14		uniss	$⊢ D \subseteq H \times H \to ⋃ D \subseteq ⋃ (H \times H)$
15		uniss	$⊢ ⋃ D \subseteq ⋃ (H \times H) \to ⋃ ⋃ D \subseteq ⋃ ⋃ (H \times H)$
16	13 14 15	mp2b	$⊢ ⋃ ⋃ D \subseteq ⋃ ⋃ (H \times H)$
17		unixpss	$⊢ ⋃ ⋃ (H \times H) \subseteq H \cup H$
18		unidm	$⊢ H \cup H = H$
19	17 18	sseqtri	$⊢ ⋃ ⋃ (H \times H) \subseteq H$
20	16 19	sstri	$⊢ ⋃ ⋃ D \subseteq H$
21	12 20	eqssi	$⊢ H = ⋃ ⋃ D$
22		filelss	$⊢ (F \in Fil (X) \land n \in F) \to n \subseteq X$
23		xpss2	$⊢ n \subseteq X \to \{n\} \times n \subseteq \{n\} \times X$
24	22 23	syl	$⊢ (F \in Fil (X) \land n \in F) \to \{n\} \times n \subseteq \{n\} \times X$
25	24	ralrimiva	$⊢ F \in Fil (X) \to \forall n \in F \{n\} \times n \subseteq \{n\} \times X$
26		ss2iun	$⊢ \forall n \in F \{n\} \times n \subseteq \{n\} \times X \to ⋃_{n \in F} (\{n\} \times n) \subseteq ⋃_{n \in F} (\{n\} \times X)$
27	25 26	syl	$⊢ F \in Fil (X) \to ⋃_{n \in F} (\{n\} \times n) \subseteq ⋃_{n \in F} (\{n\} \times X)$
28		iunxpconst	$⊢ ⋃_{n \in F} (\{n\} \times X) = F \times X$
29	27 28	sseqtrdi	$⊢ F \in Fil (X) \to ⋃_{n \in F} (\{n\} \times n) \subseteq F \times X$
30	1 29	eqsstrid	$⊢ F \in Fil (X) \to H \subseteq F \times X$
31	5	a1i	$⊢ F \in Fil (X) \to {I ↾}_{H} \subseteq D$
32	2	relopabiv	$⊢ Rel D$
33	31 32	jctil	$⊢ F \in Fil (X) \to (Rel D \land {I ↾}_{H} \subseteq D)$
34		simpl	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to F \in Fil (X)$
35	30	adantr	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to H \subseteq F \times X$
36		simprl	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to v \in H$
37	35 36	sseldd	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to v \in (F \times X)$
38		xp1st	$⊢ v \in (F \times X) \to 1^{st} (v) \in F$
39	37 38	syl	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to 1^{st} (v) \in F$
40		simprr	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to z \in H$
41	35 40	sseldd	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to z \in (F \times X)$
42		xp1st	$⊢ z \in (F \times X) \to 1^{st} (z) \in F$
43	41 42	syl	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to 1^{st} (z) \in F$
44		filinn0	$⊢ (F \in Fil (X) \land 1^{st} (v) \in F \land 1^{st} (z) \in F) \to 1^{st} (v) \cap 1^{st} (z) \neq \emptyset$
45	34 39 43 44	syl3anc	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to 1^{st} (v) \cap 1^{st} (z) \neq \emptyset$
46		n0	$⊢ 1^{st} (v) \cap 1^{st} (z) \neq \emptyset \leftrightarrow \exists u u \in (1^{st} (v) \cap 1^{st} (z))$
47	45 46	sylib	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to \exists u u \in (1^{st} (v) \cap 1^{st} (z))$
48	36	adantr	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to v \in H$
49		filin	$⊢ (F \in Fil (X) \land 1^{st} (v) \in F \land 1^{st} (z) \in F) \to 1^{st} (v) \cap 1^{st} (z) \in F$
50	34 39 43 49	syl3anc	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to 1^{st} (v) \cap 1^{st} (z) \in F$
51	50	adantr	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to 1^{st} (v) \cap 1^{st} (z) \in F$
52		simpr	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to u \in (1^{st} (v) \cap 1^{st} (z))$
53		id	$⊢ n = 1^{st} (v) \cap 1^{st} (z) \to n = 1^{st} (v) \cap 1^{st} (z)$
54	53	opeliunxp2	$⊢ ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in ⋃_{n \in F} (\{n\} \times n) \leftrightarrow (1^{st} (v) \cap 1^{st} (z) \in F \land u \in (1^{st} (v) \cap 1^{st} (z)))$
55	51 52 54	sylanbrc	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in ⋃_{n \in F} (\{n\} \times n)$
56	55 1	eleqtrrdi	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in H$
57		fvex	$⊢ 1^{st} (v) \in V$
58	57	inex1	$⊢ 1^{st} (v) \cap 1^{st} (z) \in V$
59		vex	$⊢ u \in V$
60	58 59	op1st	$⊢ 1^{st} (⟨1^{st} (v) \cap 1^{st} (z), u⟩) = 1^{st} (v) \cap 1^{st} (z)$
61		inss1	$⊢ 1^{st} (v) \cap 1^{st} (z) \subseteq 1^{st} (v)$
62	60 61	eqsstri	$⊢ 1^{st} (⟨1^{st} (v) \cap 1^{st} (z), u⟩) \subseteq 1^{st} (v)$
63		vex	$⊢ v \in V$
64		opex	$⊢ ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in V$
65	1 2 63 64	filnetlem1	$⊢ v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \leftrightarrow ((v \in H \land ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in H) \land 1^{st} (⟨1^{st} (v) \cap 1^{st} (z), u⟩) \subseteq 1^{st} (v))$
66	62 65	mpbiran2	$⊢ v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \leftrightarrow (v \in H \land ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in H)$
67	48 56 66	sylanbrc	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩$
68	40	adantr	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to z \in H$
69		inss2	$⊢ 1^{st} (v) \cap 1^{st} (z) \subseteq 1^{st} (z)$
70	60 69	eqsstri	$⊢ 1^{st} (⟨1^{st} (v) \cap 1^{st} (z), u⟩) \subseteq 1^{st} (z)$
71		vex	$⊢ z \in V$
72	1 2 71 64	filnetlem1	$⊢ z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \leftrightarrow ((z \in H \land ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in H) \land 1^{st} (⟨1^{st} (v) \cap 1^{st} (z), u⟩) \subseteq 1^{st} (z))$
73	70 72	mpbiran2	$⊢ z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \leftrightarrow (z \in H \land ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \in H)$
74	68 56 73	sylanbrc	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩$
75		breq2	$⊢ w = ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \to (v D w \leftrightarrow v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩)$
76		breq2	$⊢ w = ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \to (z D w \leftrightarrow z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩)$
77	75 76	anbi12d	$⊢ w = ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \to ((v D w \land z D w) \leftrightarrow (v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \land z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩))$
78	64 77	spcev	$⊢ (v D ⟨1^{st} (v) \cap 1^{st} (z), u⟩ \land z D ⟨1^{st} (v) \cap 1^{st} (z), u⟩) \to \exists w (v D w \land z D w)$
79	67 74 78	syl2anc	$⊢ ((F \in Fil (X) \land (v \in H \land z \in H)) \land u \in (1^{st} (v) \cap 1^{st} (z))) \to \exists w (v D w \land z D w)$
80	47 79	exlimddv	$⊢ (F \in Fil (X) \land (v \in H \land z \in H)) \to \exists w (v D w \land z D w)$
81	80	ralrimivva	$⊢ F \in Fil (X) \to \forall v \in H \forall z \in H \exists w (v D w \land z D w)$
82		codir	$⊢ H \times H \subseteq D^{-1} \circ D \leftrightarrow \forall v \in H \forall z \in H \exists w (v D w \land z D w)$
83	81 82	sylibr	$⊢ F \in Fil (X) \to H \times H \subseteq D^{-1} \circ D$
84		vex	$⊢ w \in V$
85	1 2 63 84	filnetlem1	$⊢ v D w \leftrightarrow ((v \in H \land w \in H) \land 1^{st} (w) \subseteq 1^{st} (v))$
86	85	simplbi	$⊢ v D w \to (v \in H \land w \in H)$
87	86	simpld	$⊢ v D w \to v \in H$
88	1 2 84 71	filnetlem1	$⊢ w D z \leftrightarrow ((w \in H \land z \in H) \land 1^{st} (z) \subseteq 1^{st} (w))$
89	88	simplbi	$⊢ w D z \to (w \in H \land z \in H)$
90	89	simprd	$⊢ w D z \to z \in H$
91	87 90	anim12i	$⊢ (v D w \land w D z) \to (v \in H \land z \in H)$
92	88	simprbi	$⊢ w D z \to 1^{st} (z) \subseteq 1^{st} (w)$
93	85	simprbi	$⊢ v D w \to 1^{st} (w) \subseteq 1^{st} (v)$
94	92 93	sylan9ssr	$⊢ (v D w \land w D z) \to 1^{st} (z) \subseteq 1^{st} (v)$
95	1 2 63 71	filnetlem1	$⊢ v D z \leftrightarrow ((v \in H \land z \in H) \land 1^{st} (z) \subseteq 1^{st} (v))$
96	91 94 95	sylanbrc	$⊢ (v D w \land w D z) \to v D z$
97	96	ax-gen	$⊢ \forall z ((v D w \land w D z) \to v D z)$
98	97	gen2	$⊢ \forall v \forall w \forall z ((v D w \land w D z) \to v D z)$
99		cotr	$⊢ D \circ D \subseteq D \leftrightarrow \forall v \forall w \forall z ((v D w \land w D z) \to v D z)$
100	98 99	mpbir	$⊢ D \circ D \subseteq D$
101	83 100	jctil	$⊢ F \in Fil (X) \to (D \circ D \subseteq D \land H \times H \subseteq D^{-1} \circ D)$
102		filtop	$⊢ F \in Fil (X) \to X \in F$
103		xpexg	$⊢ (F \in Fil (X) \land X \in F) \to F \times X \in V$
104	102 103	mpdan	$⊢ F \in Fil (X) \to F \times X \in V$
105	104 30	ssexd	$⊢ F \in Fil (X) \to H \in V$
106	105 105	xpexd	$⊢ F \in Fil (X) \to H \times H \in V$
107		ssexg	$⊢ (D \subseteq H \times H \land H \times H \in V) \to D \in V$
108	13 106 107	sylancr	$⊢ F \in Fil (X) \to D \in V$
109	21	isdir	$⊢ D \in V \to (D \in DirRel \leftrightarrow ((Rel D \land {I ↾}_{H} \subseteq D) \land (D \circ D \subseteq D \land H \times H \subseteq D^{-1} \circ D)))$
110	108 109	syl	$⊢ F \in Fil (X) \to (D \in DirRel \leftrightarrow ((Rel D \land {I ↾}_{H} \subseteq D) \land (D \circ D \subseteq D \land H \times H \subseteq D^{-1} \circ D)))$
111	33 101 110	mpbir2and	$⊢ F \in Fil (X) \to D \in DirRel$
112	30 111	jca	$⊢ F \in Fil (X) \to (H \subseteq F \times X \land D \in DirRel)$
113	21 112	pm3.2i	$⊢ (H = ⋃ ⋃ D \land (F \in Fil (X) \to (H \subseteq F \times X \land D \in DirRel)))$

Metamath Proof Explorer

Theorem filnetlem3

Proof