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 ) ) )
4 3 adantl 
 |-  ( ( 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 ) )