Metamath Proof Explorer

Theorem setsn0fun

Description: The value of the structure replacement function (without the empty set) is a function if the structure (without the empty set) is a function. (Contributed by AV, 7-Jun-2021) (Revised by AV, 16-Nov-2021)

		Ref	Expression
	Hypotheses	setsn0fun.s	$⊢ φ \to S Struct X$
		setsn0fun.i	$⊢ φ \to I \in U$
		setsn0fun.e	$⊢ φ \to E \in W$
	Assertion	setsn0fun	$⊢ φ \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\})$

Proof

Step	Hyp	Ref	Expression
1		setsn0fun.s	$⊢ φ \to S Struct X$
2		setsn0fun.i	$⊢ φ \to I \in U$
3		setsn0fun.e	$⊢ φ \to E \in W$
4		structn0fun	$⊢ S Struct X \to Fun (S ∖ \{\emptyset\})$
5		structex	$⊢ S Struct X \to S \in V$
6		setsfun0	$⊢ ((S \in V \land Fun (S ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\})$
7	5 6	sylanl1	$⊢ ((S Struct X \land Fun (S ∖ \{\emptyset\})) \land (I \in U \land E \in W)) \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\})$
8	7	expcom	$⊢ (I \in U \land E \in W) \to ((S Struct X \land Fun (S ∖ \{\emptyset\})) \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\}))$
9	2 3 8	syl2anc	$⊢ φ \to ((S Struct X \land Fun (S ∖ \{\emptyset\})) \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\}))$
10	9	com12	$⊢ (S Struct X \land Fun (S ∖ \{\emptyset\})) \to (φ \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\}))$
11	4 10	mpdan	$⊢ S Struct X \to (φ \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\}))$
12	1 11	mpcom	$⊢ φ \to Fun ((S sSet ⟨I, E⟩) ∖ \{\emptyset\})$