This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
		setsn0fun.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
		setsn0fun.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
	Assertion	setsn0fun	⊢ ( 𝜑 → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		setsn0fun.s	⊢ ( 𝜑 → 𝑆 Struct 𝑋 )
2		setsn0fun.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
3		setsn0fun.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4		structn0fun	⊢ ( 𝑆 Struct 𝑋 → Fun ( 𝑆 ∖ { ∅ } ) )
5		structex	⊢ ( 𝑆 Struct 𝑋 → 𝑆 ∈ V )
6		setsfun0	⊢ ( ( ( 𝑆 ∈ V ∧ Fun ( 𝑆 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )
7	5 6	sylanl1	⊢ ( ( ( 𝑆 Struct 𝑋 ∧ Fun ( 𝑆 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )
8	7	expcom	⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( ( 𝑆 Struct 𝑋 ∧ Fun ( 𝑆 ∖ { ∅ } ) ) → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
9	2 3 8	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 Struct 𝑋 ∧ Fun ( 𝑆 ∖ { ∅ } ) ) → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
10	9	com12	⊢ ( ( 𝑆 Struct 𝑋 ∧ Fun ( 𝑆 ∖ { ∅ } ) ) → ( 𝜑 → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
11	4 10	mpdan	⊢ ( 𝑆 Struct 𝑋 → ( 𝜑 → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ) )
12	1 11	mpcom	⊢ ( 𝜑 → Fun ( ( 𝑆 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )