Theorem discsubclem

Description: Lemma for discsubc . (Contributed by Zhi Wang, 1-Nov-2025)

	Ref	Expression
Hypothesis	discsubc.j	⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
Assertion	discsubclem	⊢ 𝐽 Fn ( 𝑆 × 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
2		snex	⊢ { ( 𝐼 ‘ 𝑥 ) } ∈ V
3		0ex	⊢ ∅ ∈ V
4	2 3	ifex	⊢ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ∈ V
5	1 4	fnmpoi	⊢ 𝐽 Fn ( 𝑆 × 𝑆 )