# 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
`|- G e. CH`
pjco.2
`|- H e. CH`
Assertion pjss1coi
`|- ( G C_ H <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )`

### Proof

Step Hyp Ref Expression
1 pjco.1
` |-  G e. CH`
2 pjco.2
` |-  H e. CH`
3 2 1 pjcoi
` |-  ( x e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` H ) ` ( ( projh ` G ) ` x ) ) )`
` |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` H ) ` ( ( projh ` G ) ` x ) ) )`
5 1 pjcli
` |-  ( x e. ~H -> ( ( projh ` G ) ` x ) e. G )`
6 ssel2
` |-  ( ( G C_ H /\ ( ( projh ` G ) ` x ) e. G ) -> ( ( projh ` G ) ` x ) e. H )`
7 5 6 sylan2
` |-  ( ( G C_ H /\ x e. ~H ) -> ( ( projh ` G ) ` x ) e. H )`
8 pjid
` |-  ( ( H e. CH /\ ( ( projh ` G ) ` x ) e. H ) -> ( ( projh ` H ) ` ( ( projh ` G ) ` x ) ) = ( ( projh ` G ) ` x ) )`
9 2 7 8 sylancr
` |-  ( ( G C_ H /\ x e. ~H ) -> ( ( projh ` H ) ` ( ( projh ` G ) ` x ) ) = ( ( projh ` G ) ` x ) )`
10 4 9 eqtrd
` |-  ( ( G C_ H /\ x e. ~H ) -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) )`
11 10 ralrimiva
` |-  ( G C_ H -> A. x e. ~H ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) )`
12 2 pjfi
` |-  ( projh ` H ) : ~H --> ~H`
13 1 pjfi
` |-  ( projh ` G ) : ~H --> ~H`
14 12 13 hocofi
` |-  ( ( projh ` H ) o. ( projh ` G ) ) : ~H --> ~H`
15 14 13 hoeqi
` |-  ( A. x e. ~H ( ( ( projh ` H ) o. ( projh ` G ) ) ` x ) = ( ( projh ` G ) ` x ) <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )`
16 11 15 sylib
` |-  ( G C_ H -> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )`
17 rneq
` |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) -> ran ( ( projh ` H ) o. ( projh ` G ) ) = ran ( projh ` G ) )`
18 rncoss
` |-  ran ( ( projh ` H ) o. ( projh ` G ) ) C_ ran ( projh ` H )`
19 17 18 eqsstrrdi
` |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) -> ran ( projh ` G ) C_ ran ( projh ` H ) )`
20 1 pjrni
` |-  ran ( projh ` G ) = G`
21 2 pjrni
` |-  ran ( projh ` H ) = H`
22 19 20 21 3sstr3g
` |-  ( ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) -> G C_ H )`
23 16 22 impbii
` |-  ( G C_ H <-> ( ( projh ` H ) o. ( projh ` G ) ) = ( projh ` G ) )`