Metamath Proof Explorer


Theorem fncoOLD

Description: Obsolete version of fnco as of 20-Sep-2024. (Contributed by NM, 22-May-2006) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion fncoOLD ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → ( 𝐹𝐺 ) Fn 𝐵 )

Proof

Step Hyp Ref Expression
1 fnfun ( 𝐹 Fn 𝐴 → Fun 𝐹 )
2 fnfun ( 𝐺 Fn 𝐵 → Fun 𝐺 )
3 funco ( ( Fun 𝐹 ∧ Fun 𝐺 ) → Fun ( 𝐹𝐺 ) )
4 1 2 3 syl2an ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ) → Fun ( 𝐹𝐺 ) )
5 4 3adant3 ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → Fun ( 𝐹𝐺 ) )
6 fndm ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
7 6 sseq2d ( 𝐹 Fn 𝐴 → ( ran 𝐺 ⊆ dom 𝐹 ↔ ran 𝐺𝐴 ) )
8 7 biimpar ( ( 𝐹 Fn 𝐴 ∧ ran 𝐺𝐴 ) → ran 𝐺 ⊆ dom 𝐹 )
9 dmcosseq ( ran 𝐺 ⊆ dom 𝐹 → dom ( 𝐹𝐺 ) = dom 𝐺 )
10 8 9 syl ( ( 𝐹 Fn 𝐴 ∧ ran 𝐺𝐴 ) → dom ( 𝐹𝐺 ) = dom 𝐺 )
11 10 3adant2 ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → dom ( 𝐹𝐺 ) = dom 𝐺 )
12 fndm ( 𝐺 Fn 𝐵 → dom 𝐺 = 𝐵 )
13 12 3ad2ant2 ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → dom 𝐺 = 𝐵 )
14 11 13 eqtrd ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → dom ( 𝐹𝐺 ) = 𝐵 )
15 df-fn ( ( 𝐹𝐺 ) Fn 𝐵 ↔ ( Fun ( 𝐹𝐺 ) ∧ dom ( 𝐹𝐺 ) = 𝐵 ) )
16 5 14 15 sylanbrc ( ( 𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ran 𝐺𝐴 ) → ( 𝐹𝐺 ) Fn 𝐵 )