Theorem filnetlem2

Description: Lemma for filnet . The field of the direction. (Contributed by Jeff Hankins, 13-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

	Ref	Expression
Hypotheses	filnet.h	$$⊢H=\bigcup _{n\in F}\left(\left\{n\right\}\times n\right)$$
	filnet.d	$$⊢D=\left\{⟨x,y⟩|\left(\left(x\in H\wedge y\in H\right)\wedge 1^{st}\left(y\right)\subseteq 1^{st}\left(x\right)\right)\right\}$$
Assertion	filnetlem2	$$⊢\left({\mathrm{I}\upharpoonright }_H\subseteq D\wedge D\subseteq H\times H\right)$$

Proof

Step	Hyp	Ref	Expression
1		filnet.h	$$⊢H=\bigcup _{n\in F}\left(\left\{n\right\}\times n\right)$$
2		filnet.d	$$⊢D=\left\{⟨x,y⟩|\left(\left(x\in H\wedge y\in H\right)\wedge 1^{st}\left(y\right)\subseteq 1^{st}\left(x\right)\right)\right\}$$
3		idref	$$⊢{\mathrm{I}\upharpoonright }_H\subseteq D\leftrightarrow \forall z\in HzDz$$
4		ssid	$$⊢1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)$$
5		vex	$$⊢z\in \mathrm{V}$$
6	1 2 5 5	filnetlem1	$$⊢zDz\leftrightarrow \left(\left(z\in H\wedge z\in H\right)\wedge 1^{st}\left(z\right)\subseteq 1^{st}\left(z\right)\right)$$
7	4 6	mpbiran2	$$⊢zDz\leftrightarrow \left(z\in H\wedge z\in H\right)$$
8	7	biimpri	$$⊢\left(z\in H\wedge z\in H\right)\to zDz$$
9	8	anidms	$$⊢z\in H\to zDz$$
10	3 9	mprgbir	$$⊢{\mathrm{I}\upharpoonright }_H\subseteq D$$
11		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in H\wedge y\in H\right)\wedge 1^{st}\left(y\right)\subseteq 1^{st}\left(x\right)\right)\right\}\subseteq H\times H$$
12	2 11	eqsstri	$$⊢D\subseteq H\times H$$
13	10 12	pm3.2i	$$⊢\left({\mathrm{I}\upharpoonright }_H\subseteq D\wedge D\subseteq H\times H\right)$$