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∈Cℋ
pjco.2 ⊢H∈Cℋ
Assertion pjss1coi ⊢G⊆H↔projℎ⁡H∘projℎ⁡G=projℎ⁡G

Proof

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