Theorem filnetlem1

Description: Lemma for filnet . Change variables. (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\}$$
	filnetlem1.a	$$⊢A\in \mathrm{V}$$
	filnetlem1.b	$$⊢B\in \mathrm{V}$$
Assertion	filnetlem1	$$⊢ADB\leftrightarrow \left(\left(A\in H\wedge B\in H\right)\wedge 1^{st}\left(B\right)\subseteq 1^{st}\left(A\right)\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		filnetlem1.a	$$⊢A\in \mathrm{V}$$
4		filnetlem1.b	$$⊢B\in \mathrm{V}$$
5		fveq2	$$⊢x=A\to 1^{st}\left(x\right)=1^{st}\left(A\right)$$
6	5	sseq2d	$$⊢x=A\to \left(1^{st}\left(y\right)\subseteq 1^{st}\left(x\right)\leftrightarrow 1^{st}\left(y\right)\subseteq 1^{st}\left(A\right)\right)$$
7		fveq2	$$⊢y=B\to 1^{st}\left(y\right)=1^{st}\left(B\right)$$
8	7	sseq1d	$$⊢y=B\to \left(1^{st}\left(y\right)\subseteq 1^{st}\left(A\right)\leftrightarrow 1^{st}\left(B\right)\subseteq 1^{st}\left(A\right)\right)$$
9	6 8	sylan9bb	$$⊢\left(x=A\wedge y=B\right)\to \left(1^{st}\left(y\right)\subseteq 1^{st}\left(x\right)\leftrightarrow 1^{st}\left(B\right)\subseteq 1^{st}\left(A\right)\right)$$
10	9 2	brab2a	$$⊢ADB\leftrightarrow \left(\left(A\in H\wedge B\in H\right)\wedge 1^{st}\left(B\right)\subseteq 1^{st}\left(A\right)\right)$$