Theorem fco3OLD

Description: Obsolete version of funcofd as 20-Sep-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fco3OLD.1	⊢ ( 𝜑 → Fun 𝐹 )
	fco3OLD.2	⊢ ( 𝜑 → Fun 𝐺 )
Assertion	fco3OLD	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fco3OLD.1	⊢ ( 𝜑 → Fun 𝐹 )
2		fco3OLD.2	⊢ ( 𝜑 → Fun 𝐺 )
3		funco	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )
4	1 2 3	syl2anc	⊢ ( 𝜑 → Fun ( 𝐹 ∘ 𝐺 ) )
5		fdmrn	⊢ ( Fun ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ran ( 𝐹 ∘ 𝐺 ) )
6	4 5	sylib	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ran ( 𝐹 ∘ 𝐺 ) )
7		dmco	⊢ dom ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 “ dom 𝐹 )
8	7	feq2i	⊢ ( ( 𝐹 ∘ 𝐺 ) : dom ( 𝐹 ∘ 𝐺 ) ⟶ ran ( 𝐹 ∘ 𝐺 ) ↔ ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran ( 𝐹 ∘ 𝐺 ) )
9	6 8	sylib	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran ( 𝐹 ∘ 𝐺 ) )
10		rncoss	⊢ ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹
11	10	a1i	⊢ ( 𝜑 → ran ( 𝐹 ∘ 𝐺 ) ⊆ ran 𝐹 )
12	9 11	fssd	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐺 ) : ( ◡ 𝐺 “ dom 𝐹 ) ⟶ ran 𝐹 )