setsfun

Description: A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021)

		Ref	Expression
	Assertion	setsfun	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to Fun (G sSet ⟨I, E⟩)$

Proof

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun G \to Fun ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})})$
2	1	adantl	$⊢ (G \in V \land Fun G) \to Fun ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})})$
3	2	adantr	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to Fun ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})})$
4		funsng	$⊢ (I \in U \land E \in W) \to Fun \{⟨I, E⟩\}$
5	4	adantl	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to Fun \{⟨I, E⟩\}$
6		dmres	$⊢ dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) = (V ∖ dom \{⟨I, E⟩\}) \cap dom G$
7	6	ineq1i	$⊢ dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = ((V ∖ dom \{⟨I, E⟩\}) \cap dom G) \cap dom \{⟨I, E⟩\}$
8		in32	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom G) \cap dom \{⟨I, E⟩\} = ((V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\}) \cap dom G$
9		incom	$⊢ (V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\} = dom \{⟨I, E⟩\} \cap (V ∖ dom \{⟨I, E⟩\})$
10		disjdif	$⊢ dom \{⟨I, E⟩\} \cap (V ∖ dom \{⟨I, E⟩\}) = \emptyset$
11	9 10	eqtri	$⊢ (V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\} = \emptyset$
12	11	ineq1i	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\}) \cap dom G = \emptyset \cap dom G$
13		0in	$⊢ \emptyset \cap dom G = \emptyset$
14	8 12 13	3eqtri	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom G) \cap dom \{⟨I, E⟩\} = \emptyset$
15	7 14	eqtri	$⊢ dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset$
16	15	a1i	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset$
17		funun	$⊢ ((Fun ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \land Fun \{⟨I, E⟩\}) \land dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset) \to Fun (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\})$
18	3 5 16 17	syl21anc	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to Fun (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\})$
19		opex	$⊢ ⟨I, E⟩ \in V$
20	19	a1i	$⊢ Fun G \to ⟨I, E⟩ \in V$
21		setsvalg	$⊢ (G \in V \land ⟨I, E⟩ \in V) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
22	20 21	sylan2	$⊢ (G \in V \land Fun G) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
23	22	funeqd	$⊢ (G \in V \land Fun G) \to (Fun (G sSet ⟨I, E⟩) \leftrightarrow Fun (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}))$
24	23	adantr	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to (Fun (G sSet ⟨I, E⟩) \leftrightarrow Fun (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}))$
25	18 24	mpbird	$⊢ ((G \in V \land Fun G) \land (I \in U \land E \in W)) \to Fun (G sSet ⟨I, E⟩)$

Metamath Proof Explorer

Theorem setsfun

Proof