Theorem iinfconstbaslem

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

	Ref	Expression
Hypotheses	discsubc.j	⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
	discsubc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	discsubc.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
	discsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	discsubc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	iinfconstbas.a	⊢ ( 𝜑 → 𝐴 = ( ( Subcat ‘ 𝐶 ) ∩ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ) )
Assertion	iinfconstbaslem	⊢ ( 𝜑 → 𝐽 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		discsubc.j	⊢ 𝐽 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
2		discsubc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		discsubc.i	⊢ 𝐼 = ( Id ‘ 𝐶 )
4		discsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
5		discsubc.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
6		iinfconstbas.a	⊢ ( 𝜑 → 𝐴 = ( ( Subcat ‘ 𝐶 ) ∩ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ) )
7	1 2 3 4 5	discsubc	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
8	1	discsubclem	⊢ 𝐽 Fn ( 𝑆 × 𝑆 )
9	8	a1i	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
10		fneq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 Fn ( 𝑆 × 𝑆 ) ↔ 𝐽 Fn ( 𝑆 × 𝑆 ) ) )
11	7 9 10	elabd	⊢ ( 𝜑 → 𝐽 ∈ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } )
12	7 11	elind	⊢ ( 𝜑 → 𝐽 ∈ ( ( Subcat ‘ 𝐶 ) ∩ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ) )
13	12 6	eleqtrrd	⊢ ( 𝜑 → 𝐽 ∈ 𝐴 )