This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fresaunres1

Description: From the union of two functions that agree on the domain overlap, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Assertion fresaunres1 ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 )
2 1 reseq1i ⊢ ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 )
3 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
4 3 reseq2i ⊢ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) )
5 3 reseq2i ⊢ ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) )
6 4 5 eqeq12i ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) )
7 eqcom ⊢ ( ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) ↔ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) )
8 6 7 bitri ⊢ ( ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) )
9 fresaunres2 ⊢ ( ( 𝐺 : 𝐵 ⟶ 𝐶 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ∧ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
10 9 3com12 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐺 ↾ ( 𝐵 ∩ 𝐴 ) ) = ( 𝐹 ↾ ( 𝐵 ∩ 𝐴 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
11 8 10 syl3an3b ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐺 ∪ 𝐹 ) ↾ 𝐴 ) = 𝐹 )
12 2 11 eqtrid ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ 𝐺 : 𝐵 ⟶ 𝐶 ∧ ( 𝐹 ↾ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐺 ↾ ( 𝐴 ∩ 𝐵 ) ) ) → ( ( 𝐹 ∪ 𝐺 ) ↾ 𝐴 ) = 𝐹 )