# 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 ${⊢}{\phi }\to {S}\mathrm{Struct}{X}$
setsn0fun.i ${⊢}{\phi }\to {I}\in {U}$
setsn0fun.e ${⊢}{\phi }\to {E}\in {W}$
Assertion setsn0fun ${⊢}{\phi }\to \mathrm{Fun}\left(\left({S}\mathrm{sSet}⟨{I},{E}⟩\right)\setminus \left\{\varnothing \right\}\right)$

### Proof

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