Theorem fsnunfv 7135

Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.)

Assertion

Ref	Expression
fsnunfv	⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)

Proof of Theorem fsnunfv

Step	Hyp	Ref	Expression
1		dmres 5971	. . . . . . . . 9 ⊢ dom (𝐹 ↾ {𝑋}) = ({𝑋} ∩ dom 𝐹)
2		incom 4141	. . . . . . . . 9 ⊢ ({𝑋} ∩ dom 𝐹) = (dom 𝐹 ∩ {𝑋})
3	1, 2	eqtri 2764	. . . . . . . 8 ⊢ dom (𝐹 ↾ {𝑋}) = (dom 𝐹 ∩ {𝑋})
4		disjsn 4646	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ {𝑋}) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹)
5	4	biimpri 230	. . . . . . . 8 ⊢ (¬ 𝑋 ∈ dom 𝐹 → (dom 𝐹 ∩ {𝑋}) = ∅)
6	3, 5	eqtrid 2788	. . . . . . 7 ⊢ (¬ 𝑋 ∈ dom 𝐹 → dom (𝐹 ↾ {𝑋}) = ∅)
7	6	3ad2ant3 1142	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → dom (𝐹 ↾ {𝑋}) = ∅)
8		relres 5964	. . . . . . 7 ⊢ Rel (𝐹 ↾ {𝑋})
9		reldm0 5877	. . . . . . 7 ⊢ (Rel (𝐹 ↾ {𝑋}) → ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅))
10	8, 9	ax-mp 5	. . . . . 6 ⊢ ((𝐹 ↾ {𝑋}) = ∅ ↔ dom (𝐹 ↾ {𝑋}) = ∅)
11	7, 10	sylibr 236	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ {𝑋}) = ∅)
12		fnsng 6541	. . . . . . 7 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → {⟨𝑋, 𝑌⟩} Fn {𝑋})
13	12	3adant3 1139	. . . . . 6 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → {⟨𝑋, 𝑌⟩} Fn {𝑋})
14		fnresdm 6608	. . . . . 6 ⊢ ({⟨𝑋, 𝑌⟩} Fn {𝑋} → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩})
15	13, 14	syl 17	. . . . 5 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩} ↾ {𝑋}) = {⟨𝑋, 𝑌⟩})
16	11, 15	uneq12d 4102	. . . 4 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋})) = (∅ ∪ {⟨𝑋, 𝑌⟩}))
17		resundir 5953	. . . 4 ⊢ ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = ((𝐹 ↾ {𝑋}) ∪ ({⟨𝑋, 𝑌⟩} ↾ {𝑋}))
18		uncom 4091	. . . . 5 ⊢ (∅ ∪ {⟨𝑋, 𝑌⟩}) = ({⟨𝑋, 𝑌⟩} ∪ ∅)
19		un0 4325	. . . . 5 ⊢ ({⟨𝑋, 𝑌⟩} ∪ ∅) = {⟨𝑋, 𝑌⟩}
20	18, 19	eqtr2i 2765	. . . 4 ⊢ {⟨𝑋, 𝑌⟩} = (∅ ∪ {⟨𝑋, 𝑌⟩})
21	16, 17, 20	3eqtr4g 2801	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋}) = {⟨𝑋, 𝑌⟩})
22	21	fveq1d 6833	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ({⟨𝑋, 𝑌⟩}‘𝑋))
23		snidg 4595	. . . 4 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋})
24	23	3ad2ant1 1140	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → 𝑋 ∈ {𝑋})
25	24	fvresd 6851	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → (((𝐹 ∪ {⟨𝑋, 𝑌⟩}) ↾ {𝑋})‘𝑋) = ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋))
26		fvsng 7128	. . 3 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌)
27	26	3adant3 1139	. 2 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ({⟨𝑋, 𝑌⟩}‘𝑋) = 𝑌)
28	22, 25, 27	3eqtr3d 2784	1 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ ¬ 𝑋 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑋, 𝑌⟩})‘𝑋) = 𝑌)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ w3a 1093   = wceq 1548   ∈ wcel 2121   ∪ cun 3883   ∩ cin 3884  ∅c0 4264  {csn 4558  ⟨cop 4564  dom cdm 5621   ↾ cres 5623  Rel wrel 5626   Fn wfn 6484  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-res 5633  df-iota 6445  df-fun 6491  df-fn 6492  df-fv 6497

This theorem is referenced by:  f1ounsn  7220  hashf1lem1  14412  cats1un  14678  fvsetsid  17133  islindf4  21817  wlkp1lem3  29764  wlkp1lem7  29768  wlkp1lem8  29769  eupth2eucrct  30309  evlextv  33738  mapfzcons2  43183  fnchoice  45492  nnsum4primeseven  48305  nnsum4primesevenALTV  48306  isubgr3stgrlem3  48473