Metamath Proof Explorer


Theorem elmapresaunres2

Description: fresaunres2 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014)

Ref Expression
Assertion elmapresaunres2 ( ( 𝐹 ∈ ( 𝐶m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐺 ↾ ( 𝐴𝐵 ) ) ) → ( ( 𝐹𝐺 ) ↾ 𝐵 ) = 𝐺 )

Proof

Step Hyp Ref Expression
1 elmapi ( 𝐹 ∈ ( 𝐶m 𝐴 ) → 𝐹 : 𝐴𝐶 )
2 elmapi ( 𝐺 ∈ ( 𝐶m 𝐵 ) → 𝐺 : 𝐵𝐶 )
3 id ( ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐺 ↾ ( 𝐴𝐵 ) ) → ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐺 ↾ ( 𝐴𝐵 ) ) )
4 fresaunres2 ( ( 𝐹 : 𝐴𝐶𝐺 : 𝐵𝐶 ∧ ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐺 ↾ ( 𝐴𝐵 ) ) ) → ( ( 𝐹𝐺 ) ↾ 𝐵 ) = 𝐺 )
5 1 2 3 4 syl3an ( ( 𝐹 ∈ ( 𝐶m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴𝐵 ) ) = ( 𝐺 ↾ ( 𝐴𝐵 ) ) ) → ( ( 𝐹𝐺 ) ↾ 𝐵 ) = 𝐺 )