Metamath Proof Explorer


Theorem 1stcof

Description: Composition of the first member function with another function. (Contributed by NM, 12-Oct-2007)

Ref Expression
Assertion 1stcof ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1st𝐹 ) : 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 fo1st 1st : V –onto→ V
2 fofn ( 1st : V –onto→ V → 1st Fn V )
3 1 2 ax-mp 1st Fn V
4 ffn ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 Fn 𝐴 )
5 dffn2 ( 𝐹 Fn 𝐴𝐹 : 𝐴 ⟶ V )
6 4 5 sylib ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → 𝐹 : 𝐴 ⟶ V )
7 fnfco ( ( 1st Fn V ∧ 𝐹 : 𝐴 ⟶ V ) → ( 1st𝐹 ) Fn 𝐴 )
8 3 6 7 sylancr ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1st𝐹 ) Fn 𝐴 )
9 rnco ran ( 1st𝐹 ) = ran ( 1st ↾ ran 𝐹 )
10 frn ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) )
11 ssres2 ( ran 𝐹 ⊆ ( 𝐵 × 𝐶 ) → ( 1st ↾ ran 𝐹 ) ⊆ ( 1st ↾ ( 𝐵 × 𝐶 ) ) )
12 rnss ( ( 1st ↾ ran 𝐹 ) ⊆ ( 1st ↾ ( 𝐵 × 𝐶 ) ) → ran ( 1st ↾ ran 𝐹 ) ⊆ ran ( 1st ↾ ( 𝐵 × 𝐶 ) ) )
13 10 11 12 3syl ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1st ↾ ran 𝐹 ) ⊆ ran ( 1st ↾ ( 𝐵 × 𝐶 ) ) )
14 f1stres ( 1st ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐵
15 frn ( ( 1st ↾ ( 𝐵 × 𝐶 ) ) : ( 𝐵 × 𝐶 ) ⟶ 𝐵 → ran ( 1st ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐵 )
16 14 15 ax-mp ran ( 1st ↾ ( 𝐵 × 𝐶 ) ) ⊆ 𝐵
17 13 16 sstrdi ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1st ↾ ran 𝐹 ) ⊆ 𝐵 )
18 9 17 eqsstrid ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ran ( 1st𝐹 ) ⊆ 𝐵 )
19 df-f ( ( 1st𝐹 ) : 𝐴𝐵 ↔ ( ( 1st𝐹 ) Fn 𝐴 ∧ ran ( 1st𝐹 ) ⊆ 𝐵 ) )
20 8 18 19 sylanbrc ( 𝐹 : 𝐴 ⟶ ( 𝐵 × 𝐶 ) → ( 1st𝐹 ) : 𝐴𝐵 )