Theorem fresaunres1 6755

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.)

Assertion

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

Proof of Theorem fresaunres1

Step	Hyp	Ref	Expression
1		uncom 4157	. . 3 ⊢ (𝐹 ∪ 𝐺) = (𝐺 ∪ 𝐹)
2	1	reseq1i 5965	. 2 ⊢ ((𝐹 ∪ 𝐺) ↾ 𝐴) = ((𝐺 ∪ 𝐹) ↾ 𝐴)
3		incom 4106	. . . . . 6 ⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴)
4	3	reseq2i 5966	. . . . 5 ⊢ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐹 ↾ (𝐵 ∩ 𝐴))
5	3	reseq2i 5966	. . . . 5 ⊢ (𝐺 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐵 ∩ 𝐴))
6	4, 5	eqeq12i 2778	. . . 4 ⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵)) ↔ (𝐹 ↾ (𝐵 ∩ 𝐴)) = (𝐺 ↾ (𝐵 ∩ 𝐴)))
7		eqcom 2767	. . . 4 ⊢ ((𝐹 ↾ (𝐵 ∩ 𝐴)) = (𝐺 ↾ (𝐵 ∩ 𝐴)) ↔ (𝐺 ↾ (𝐵 ∩ 𝐴)) = (𝐹 ↾ (𝐵 ∩ 𝐴)))
8	6, 7	bitri 278	. . 3 ⊢ ((𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵)) ↔ (𝐺 ↾ (𝐵 ∩ 𝐴)) = (𝐹 ↾ (𝐵 ∩ 𝐴)))
9		fresaunres2 6754	. . . 4 ⊢ ((𝐺:𝐵⟶𝐶 ∧ 𝐹:𝐴⟶𝐶 ∧ (𝐺 ↾ (𝐵 ∩ 𝐴)) = (𝐹 ↾ (𝐵 ∩ 𝐴))) → ((𝐺 ∪ 𝐹) ↾ 𝐴) = 𝐹)
10	9	3com12 1141	. . 3 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐺 ↾ (𝐵 ∩ 𝐴)) = (𝐹 ↾ (𝐵 ∩ 𝐴))) → ((𝐺 ∪ 𝐹) ↾ 𝐴) = 𝐹)
11	8, 10	syl3an3b 1432	. 2 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐺 ∪ 𝐹) ↾ 𝐴) = 𝐹)
12	2, 11	eqtrid 2807	1 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐶 ∧ (𝐹 ↾ (𝐴 ∩ 𝐵)) = (𝐺 ↾ (𝐴 ∩ 𝐵))) → ((𝐹 ∪ 𝐺) ↾ 𝐴) = 𝐹)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103   = wceq 1569   ∩ cin 4089   ∪ cun 4149   ↾ cres 5652  ⟶wf 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-dm 5660  df-res 5662  df-fun 6540  df-fn 6541  df-f 6542

This theorem is used by:  mapunen  9165  hashf1lem1  14600  ptuncnv  24126  resf1o  33322  cvmliftlem10  36059  aacllem  50939