Theorem iinfconstbaslem

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

	Ref	Expression
Hypotheses	discsubc.j	|- J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
	discsubc.b	|- B = ( Base ` C )
	discsubc.i	|- I = ( Id ` C )
	discsubc.s	|- ( ph -> S C_ B )
	discsubc.c	|- ( ph -> C e. Cat )
	iinfconstbas.a	|- ( ph -> A = ( ( Subcat ` C ) i^i { j | j Fn ( S X. S ) } ) )
Assertion	iinfconstbaslem	|- ( ph -> J e. A )

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	|- J = ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) )
2		discsubc.b	|- B = ( Base ` C )
3		discsubc.i	|- I = ( Id ` C )
4		discsubc.s	|- ( ph -> S C_ B )
5		discsubc.c	|- ( ph -> C e. Cat )
6		iinfconstbas.a	|- ( ph -> A = ( ( Subcat ` C ) i^i { j | j Fn ( S X. S ) } ) )
7	1 2 3 4 5	discsubc	|- ( ph -> J e. ( Subcat ` C ) )
8	1	discsubclem	|- J Fn ( S X. S )
9	8	a1i	|- ( ph -> J Fn ( S X. S ) )
10		fneq1	|- ( j = J -> ( j Fn ( S X. S ) <-> J Fn ( S X. S ) ) )
11	7 9 10	elabd	|- ( ph -> J e. { j | j Fn ( S X. S ) } )
12	7 11	elind	|- ( ph -> J e. ( ( Subcat ` C ) i^i { j | j Fn ( S X. S ) } ) )
13	12 6	eleqtrrd	|- ( ph -> J e. A )