fvsetsid

Description: The value of the structure replacement function for its first argument is its second argument. (Contributed by SO, 12-Jul-2018)

		Ref	Expression
	Assertion	fvsetsid	$⊢ (F \in V \land X \in W \land Y \in U) \to (F sSet ⟨X, Y⟩) (X) = Y$

Step	Hyp	Ref	Expression
1		setsval	$⊢ (F \in V \land Y \in U) \to F sSet ⟨X, Y⟩ = ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, Y⟩\}$
2	1	3adant2	$⊢ (F \in V \land X \in W \land Y \in U) \to F sSet ⟨X, Y⟩ = ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, Y⟩\}$
3	2	fveq1d	$⊢ (F \in V \land X \in W \land Y \in U) \to (F sSet ⟨X, Y⟩) (X) = (({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, Y⟩\}) (X)$
4		simp2	$⊢ (F \in V \land X \in W \land Y \in U) \to X \in W$
5		simp3	$⊢ (F \in V \land X \in W \land Y \in U) \to Y \in U$
6		neldifsn	$⊢ \neg X \in (V ∖ \{X\})$
7		dmres	$⊢ dom ({F ↾}_{(V ∖ \{X\})}) = (V ∖ \{X\}) \cap dom F$
8		inss1	$⊢ (V ∖ \{X\}) \cap dom F \subseteq V ∖ \{X\}$
9	7 8	eqsstri	$⊢ dom ({F ↾}_{(V ∖ \{X\})}) \subseteq V ∖ \{X\}$
10	9	sseli	$⊢ X \in dom ({F ↾}_{(V ∖ \{X\})}) \to X \in (V ∖ \{X\})$
11	6 10	mto	$⊢ \neg X \in dom ({F ↾}_{(V ∖ \{X\})})$
12	11	a1i	$⊢ (F \in V \land X \in W \land Y \in U) \to \neg X \in dom ({F ↾}_{(V ∖ \{X\})})$
13		fsnunfv	$⊢ (X \in W \land Y \in U \land \neg X \in dom ({F ↾}_{(V ∖ \{X\})})) \to (({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, Y⟩\}) (X) = Y$
14	4 5 12 13	syl3anc	$⊢ (F \in V \land X \in W \land Y \in U) \to (({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, Y⟩\}) (X) = Y$
15	3 14	eqtrd	$⊢ (F \in V \land X \in W \land Y \in U) \to (F sSet ⟨X, Y⟩) (X) = Y$

Metamath Proof Explorer