# Metamath Proof Explorer

## Theorem pjss1coi

Description: Subset relationship for projections. Theorem 4.5(i)<->(iii) of Beran p. 112. (Contributed by NM, 1-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 𝐺C
pjco.2 𝐻C
Assertion pjss1coi ( 𝐺𝐻 ↔ ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) )

### Proof

Step Hyp Ref Expression
1 pjco.1 𝐺C
2 pjco.2 𝐻C
3 2 1 pjcoi ( 𝑥 ∈ ℋ → ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ‘ 𝑥 ) = ( ( proj𝐻 ) ‘ ( ( proj𝐺 ) ‘ 𝑥 ) ) )
4 3 adantl ( ( 𝐺𝐻𝑥 ∈ ℋ ) → ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ‘ 𝑥 ) = ( ( proj𝐻 ) ‘ ( ( proj𝐺 ) ‘ 𝑥 ) ) )
5 1 pjcli ( 𝑥 ∈ ℋ → ( ( proj𝐺 ) ‘ 𝑥 ) ∈ 𝐺 )
6 ssel2 ( ( 𝐺𝐻 ∧ ( ( proj𝐺 ) ‘ 𝑥 ) ∈ 𝐺 ) → ( ( proj𝐺 ) ‘ 𝑥 ) ∈ 𝐻 )
7 5 6 sylan2 ( ( 𝐺𝐻𝑥 ∈ ℋ ) → ( ( proj𝐺 ) ‘ 𝑥 ) ∈ 𝐻 )
8 pjid ( ( 𝐻C ∧ ( ( proj𝐺 ) ‘ 𝑥 ) ∈ 𝐻 ) → ( ( proj𝐻 ) ‘ ( ( proj𝐺 ) ‘ 𝑥 ) ) = ( ( proj𝐺 ) ‘ 𝑥 ) )
9 2 7 8 sylancr ( ( 𝐺𝐻𝑥 ∈ ℋ ) → ( ( proj𝐻 ) ‘ ( ( proj𝐺 ) ‘ 𝑥 ) ) = ( ( proj𝐺 ) ‘ 𝑥 ) )
10 4 9 eqtrd ( ( 𝐺𝐻𝑥 ∈ ℋ ) → ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ‘ 𝑥 ) = ( ( proj𝐺 ) ‘ 𝑥 ) )
11 10 ralrimiva ( 𝐺𝐻 → ∀ 𝑥 ∈ ℋ ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ‘ 𝑥 ) = ( ( proj𝐺 ) ‘ 𝑥 ) )
12 2 pjfi ( proj𝐻 ) : ℋ ⟶ ℋ
13 1 pjfi ( proj𝐺 ) : ℋ ⟶ ℋ
14 12 13 hocofi ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) : ℋ ⟶ ℋ
15 14 13 hoeqi ( ∀ 𝑥 ∈ ℋ ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ‘ 𝑥 ) = ( ( proj𝐺 ) ‘ 𝑥 ) ↔ ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) )
16 11 15 sylib ( 𝐺𝐻 → ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) )
17 rneq ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) → ran ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ran ( proj𝐺 ) )
18 rncoss ran ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) ⊆ ran ( proj𝐻 )
19 17 18 eqsstrrdi ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) → ran ( proj𝐺 ) ⊆ ran ( proj𝐻 ) )
20 1 pjrni ran ( proj𝐺 ) = 𝐺
21 2 pjrni ran ( proj𝐻 ) = 𝐻
22 19 20 21 3sstr3g ( ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) → 𝐺𝐻 )
23 16 22 impbii ( 𝐺𝐻 ↔ ( ( proj𝐻 ) ∘ ( proj𝐺 ) ) = ( proj𝐺 ) )