Theorem discsubclem

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

	Ref	Expression
Hypothesis	discsubc.j	|- J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
Assertion	discsubclem	|- J Fn ( S X. S )

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	|- J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
2		snex	|- { ( I ` x ) } e. _V
3		0ex	|- (/) e. _V
4	2 3	ifex	|- if ( x = y , { ( I ` x ) } , (/) ) e. _V
5	1 4	fnmpoi	|- J Fn ( S X. S )