Metamath Proof Explorer


Theorem pjcofni

Description: Functionality of composition of projections. (Contributed by NM, 1-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 G C
pjco.2 H C
Assertion pjcofni proj G proj H Fn

Proof

Step Hyp Ref Expression
1 pjco.1 G C
2 pjco.2 H C
3 1 pjfi proj G :
4 2 pjfi proj H :
5 3 4 hocofni proj G proj H Fn