setsdm

Description: The domain of a structure with replacement is the domain of the original structure extended by the index of the replacement. (Contributed by AV, 7-Jun-2021)

		Ref	Expression
	Assertion	setsdm	$⊢ (G \in V \land E \in W) \to dom (G sSet ⟨I, E⟩) = dom G \cup \{I\}$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨I, E⟩ \in V$
2	1	a1i	$⊢ E \in W \to ⟨I, E⟩ \in V$
3		setsvalg	$⊢ (G \in V \land ⟨I, E⟩ \in V) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
4	2 3	sylan2	$⊢ (G \in V \land E \in W) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
5	4	dmeqd	$⊢ (G \in V \land E \in W) \to dom (G sSet ⟨I, E⟩) = dom (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\})$
6		dmun	$⊢ dom (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) = dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup dom \{⟨I, E⟩\}$
7		dmres	$⊢ dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) = (V ∖ dom \{⟨I, E⟩\}) \cap dom G$
8		dmsnopg	$⊢ E \in W \to dom \{⟨I, E⟩\} = \{I\}$
9	8	adantl	$⊢ (G \in V \land E \in W) \to dom \{⟨I, E⟩\} = \{I\}$
10	9	difeq2d	$⊢ (G \in V \land E \in W) \to V ∖ dom \{⟨I, E⟩\} = V ∖ \{I\}$
11	10	ineq1d	$⊢ (G \in V \land E \in W) \to (V ∖ dom \{⟨I, E⟩\}) \cap dom G = (V ∖ \{I\}) \cap dom G$
12		incom	$⊢ (V ∖ \{I\}) \cap dom G = dom G \cap (V ∖ \{I\})$
13		invdif	$⊢ dom G \cap (V ∖ \{I\}) = dom G ∖ \{I\}$
14	12 13	eqtri	$⊢ (V ∖ \{I\}) \cap dom G = dom G ∖ \{I\}$
15	11 14	eqtrdi	$⊢ (G \in V \land E \in W) \to (V ∖ dom \{⟨I, E⟩\}) \cap dom G = dom G ∖ \{I\}$
16	7 15	syl5eq	$⊢ (G \in V \land E \in W) \to dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) = dom G ∖ \{I\}$
17	16 9	uneq12d	$⊢ (G \in V \land E \in W) \to dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup dom \{⟨I, E⟩\} = (dom G ∖ \{I\}) \cup \{I\}$
18	6 17	syl5eq	$⊢ (G \in V \land E \in W) \to dom (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) = (dom G ∖ \{I\}) \cup \{I\}$
19		undif1	$⊢ (dom G ∖ \{I\}) \cup \{I\} = dom G \cup \{I\}$
20	19	a1i	$⊢ (G \in V \land E \in W) \to (dom G ∖ \{I\}) \cup \{I\} = dom G \cup \{I\}$
21	5 18 20	3eqtrd	$⊢ (G \in V \land E \in W) \to dom (G sSet ⟨I, E⟩) = dom G \cup \{I\}$

Metamath Proof Explorer

Theorem setsdm

Proof