Theorem pjini

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

	Ref	Expression
Hypotheses	pjocin.1	⊢ 𝐺 ∈ Cℋ
	pjocin.2	⊢ 𝐻 ∈ Cℋ
Assertion	pjini	⊢ ( 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 ∩ 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		pjocin.1	⊢ 𝐺 ∈ Cℋ
2		pjocin.2	⊢ 𝐻 ∈ Cℋ
3		inss1	⊢ ( 𝐺 ∩ 𝐻 ) ⊆ 𝐺
4	3	sseli	⊢ ( 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) → 𝐴 ∈ 𝐺 )
5		pjid	⊢ ( ( 𝐺 ∈ Cℋ ∧ 𝐴 ∈ 𝐺 ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) = 𝐴 )
6	1 4 5	sylancr	⊢ ( 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) = 𝐴 )
7	6	eleq1d	⊢ ( 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 ∩ 𝐻 ) ↔ 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) ) )
8	7	ibir	⊢ ( 𝐴 ∈ ( 𝐺 ∩ 𝐻 ) → ( ( projℎ ‘ 𝐺 ) ‘ 𝐴 ) ∈ ( 𝐺 ∩ 𝐻 ) )