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 ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 ) |