Step |
Hyp |
Ref |
Expression |
1 |
|
fco |
⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) |
2 |
|
frn |
⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ran 𝐺 ⊆ 𝐵 ) |
3 |
|
cores |
⊢ ( ran 𝐺 ⊆ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) ) |
4 |
2 3
|
syl |
⊢ ( 𝐺 : 𝐴 ⟶ 𝐵 → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) ) |
5 |
4
|
adantl |
⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) ) |
6 |
5
|
feq1d |
⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( ( ( 𝐹 ↾ 𝐵 ) ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) ) |
7 |
1 6
|
mpbid |
⊢ ( ( ( 𝐹 ↾ 𝐵 ) : 𝐵 ⟶ 𝐶 ∧ 𝐺 : 𝐴 ⟶ 𝐵 ) → ( 𝐹 ∘ 𝐺 ) : 𝐴 ⟶ 𝐶 ) |