Description: fresaunres2 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | elmapresaunres2 | ⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elmapi | ⊢ ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐶 ) | |
2 | elmapi | ⊢ ( 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) → 𝐺 : 𝐵 ⟶ 𝐶 ) | |
3 | id | ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) | |
4 | fresaunres2 | ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 ) | |
5 | 1 2 3 4 | syl3an | ⊢ ( ( 𝐹 ∈ ( 𝐶 ↑m 𝐴 ) ∧ 𝐺 ∈ ( 𝐶 ↑m 𝐵 ) ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐵 ) = 𝐺 ) |