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		disjdifr	$⊢ (V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\} = \emptyset$
10	9	ineq1i	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\}) \cap dom G = \emptyset \cap dom G$
11		0in	$⊢ \emptyset \cap dom G = \emptyset$
12	8 10 11	3eqtri	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom G) \cap dom \{⟨I, E⟩\} = \emptyset$
13	7 12	eqtri	$⊢ dom ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset$
14	13	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$
15		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⟩\})$
16	3 5 14 15	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⟩\})$
17		opex	$⊢ ⟨I, E⟩ \in V$
18	17	a1i	$⊢ Fun G \to ⟨I, E⟩ \in V$
19		setsvalg	$⊢ (G \in V \land ⟨I, E⟩ \in V) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
20	18 19	sylan2	$⊢ (G \in V \land Fun G) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
21	20	funeqd	$⊢ (G \in V \land Fun G) \to (Fun (G sSet ⟨I, E⟩) \leftrightarrow Fun (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}))$
22	21	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⟩\}))$
23	16 22	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