setsfun0

Description: A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun is useful for proofs based on isstruct2 which requires Fun ( F \ { (/) } ) for F to be an extensible structure. (Contributed by AV, 7-Jun-2021)

		Ref	Expression
	Assertion	setsfun0	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ((G sSet ⟨I, E⟩) ∖ \{\emptyset\})$

Proof

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun (G ∖ \{\emptyset\}) \to Fun ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})})$
2	1	adantl	$⊢ (G \in V \land Fun (G ∖ \{\emptyset\})) \to Fun ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})})$
3	2	adantr	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ({(G ∖ \{\emptyset\}) ↾}_{(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 ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun \{⟨I, E⟩\}$
6		dmres	$⊢ dom ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) = (V ∖ dom \{⟨I, E⟩\}) \cap dom (G ∖ \{\emptyset\})$
7	6	ineq1i	$⊢ dom ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = ((V ∖ dom \{⟨I, E⟩\}) \cap dom (G ∖ \{\emptyset\})) \cap dom \{⟨I, E⟩\}$
8		in32	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom (G ∖ \{\emptyset\})) \cap dom \{⟨I, E⟩\} = ((V ∖ dom \{⟨I, E⟩\}) \cap dom \{⟨I, E⟩\}) \cap dom (G ∖ \{\emptyset\})$
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\}) = \emptyset \cap dom (G ∖ \{\emptyset\})$
11		0in	$⊢ \emptyset \cap dom (G ∖ \{\emptyset\}) = \emptyset$
12	8 10 11	3eqtri	$⊢ ((V ∖ dom \{⟨I, E⟩\}) \cap dom (G ∖ \{\emptyset\})) \cap dom \{⟨I, E⟩\} = \emptyset$
13	7 12	eqtri	$⊢ dom ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset$
14	13	a1i	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to dom ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset$
15		funun	$⊢ ((Fun ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \land Fun \{⟨I, E⟩\}) \land dom ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cap dom \{⟨I, E⟩\} = \emptyset) \to Fun (({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\})$
16	3 5 14 15	syl21anc	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun (({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\})$
17		difundir	$⊢ (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\} = (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) ∖ \{\emptyset\}) \cup (\{⟨I, E⟩\} ∖ \{\emptyset\})$
18		resdifcom	$⊢ ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) ∖ \{\emptyset\} = {(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}$
19	18	a1i	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) ∖ \{\emptyset\} = {(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}$
20		elex	$⊢ I \in U \to I \in V$
21		elex	$⊢ E \in W \to E \in V$
22	20 21	anim12i	$⊢ (I \in U \land E \in W) \to (I \in V \land E \in V)$
23		opnz	$⊢ ⟨I, E⟩ \neq \emptyset \leftrightarrow (I \in V \land E \in V)$
24	22 23	sylibr	$⊢ (I \in U \land E \in W) \to ⟨I, E⟩ \neq \emptyset$
25	24	adantl	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to ⟨I, E⟩ \neq \emptyset$
26		disjsn2	$⊢ ⟨I, E⟩ \neq \emptyset \to \{⟨I, E⟩\} \cap \{\emptyset\} = \emptyset$
27		disjdif2	$⊢ \{⟨I, E⟩\} \cap \{\emptyset\} = \emptyset \to \{⟨I, E⟩\} ∖ \{\emptyset\} = \{⟨I, E⟩\}$
28	25 26 27	3syl	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to \{⟨I, E⟩\} ∖ \{\emptyset\} = \{⟨I, E⟩\}$
29	19 28	uneq12d	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) ∖ \{\emptyset\}) \cup (\{⟨I, E⟩\} ∖ \{\emptyset\}) = ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
30	17 29	syl5eq	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\} = ({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
31	30	funeqd	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to (Fun ((({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\}) \leftrightarrow Fun (({(G ∖ \{\emptyset\}) ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}))$
32	16 31	mpbird	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ((({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\})$
33		opex	$⊢ ⟨I, E⟩ \in V$
34	33	a1i	$⊢ Fun (G ∖ \{\emptyset\}) \to ⟨I, E⟩ \in V$
35		setsvalg	$⊢ (G \in V \land ⟨I, E⟩ \in V) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
36	34 35	sylan2	$⊢ (G \in V \land Fun (G ∖ \{\emptyset\})) \to G sSet ⟨I, E⟩ = ({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}$
37	36	difeq1d	$⊢ (G \in V \land Fun (G ∖ \{\emptyset\})) \to (G sSet ⟨I, E⟩) ∖ \{\emptyset\} = (({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\}$
38	37	funeqd	$⊢ (G \in V \land Fun (G ∖ \{\emptyset\})) \to (Fun ((G sSet ⟨I, E⟩) ∖ \{\emptyset\}) \leftrightarrow Fun ((({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\}))$
39	38	adantr	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to (Fun ((G sSet ⟨I, E⟩) ∖ \{\emptyset\}) \leftrightarrow Fun ((({G ↾}_{(V ∖ dom \{⟨I, E⟩\})}) \cup \{⟨I, E⟩\}) ∖ \{\emptyset\}))$
40	32 39	mpbird	$⊢ ((G \in V \land Fun (G ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ((G sSet ⟨I, E⟩) ∖ \{\emptyset\})$

Metamath Proof Explorer

Theorem setsfun0

Proof