Theorem pjini

Description: Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001) (New usage is discouraged.)

	Ref	Expression
Hypotheses	pjocin.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjocin.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjini	$$⊢A\in \left(G\cap H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \left(G\cap H\right)$$

Proof

Step	Hyp	Ref	Expression
1		pjocin.1	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
2		pjocin.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3		inss1	$$⊢G\cap H\subseteq G$$
4	3	sseli	$$⊢A\in \left(G\cap H\right)\to A\in G$$
5		pjid	$$⊢\left(G\in {\mathbf{C}}_{\mathscr{H}}\wedge A\in G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)=A$$
6	1 4 5	sylancr	$$⊢A\in \left(G\cap H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)=A$$
7	6	eleq1d	$$⊢A\in \left(G\cap H\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \left(G\cap H\right)\leftrightarrow A\in \left(G\cap H\right)\right)$$
8	7	ibir	$$⊢A\in \left(G\cap H\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\left(A\right)\in \left(G\cap H\right)$$