Theorem iinfconstbas

Description: The discrete category is the indexed intersection of all subcategories with the same base. (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	iinfconstbas	⊢ ( 𝜑 → 𝐽 = ( 𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 ( ℎ ‘ 𝑧 ) ) )

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 6	iinfconstbaslem	⊢ ( 𝜑 → 𝐽 ∈ 𝐴 )
8	7	ne0d	⊢ ( 𝜑 → 𝐴 ≠ ∅ )
9		iinconst	⊢ ( 𝐴 ≠ ∅ → ∩ ℎ ∈ 𝐴 𝑆 = 𝑆 )
10	8 9	syl	⊢ ( 𝜑 → ∩ ℎ ∈ 𝐴 𝑆 = 𝑆 )
11	10	eqcomd	⊢ ( 𝜑 → 𝑆 = ∩ ℎ ∈ 𝐴 𝑆 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑆 = ∩ ℎ ∈ 𝐴 𝑆 )
13	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐽 ∈ 𝐴 )
14		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ = 𝐽 ) → ℎ = 𝐽 )
15	14	oveqd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ = 𝐽 ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 𝐽 𝑦 ) )
16		snex	⊢ { ( 𝐼 ‘ 𝑥 ) } ∈ V
17		0ex	⊢ ∅ ∈ V
18	16 17	ifex	⊢ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ∈ V
19	1	ovmpt4g	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ∈ V ) → ( 𝑥 𝐽 𝑦 ) = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
20	18 19	mp3an3	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐽 𝑦 ) = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
21	20	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ = 𝐽 ) → ( 𝑥 𝐽 𝑦 ) = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
22	15 21	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ = 𝐽 ) → ( 𝑥 ℎ 𝑦 ) = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
23		sseq1	⊢ ( { ( 𝐼 ‘ 𝑥 ) } = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) → ( { ( 𝐼 ‘ 𝑥 ) } ⊆ ( 𝑥 ℎ 𝑦 ) ↔ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ⊆ ( 𝑥 ℎ 𝑦 ) ) )
24		sseq1	⊢ ( ∅ = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) → ( ∅ ⊆ ( 𝑥 ℎ 𝑦 ) ↔ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ⊆ ( 𝑥 ℎ 𝑦 ) ) )
25		simpr	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ ∈ 𝐴 )
26	6	adantr	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → 𝐴 = ( ( Subcat ‘ 𝐶 ) ∩ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ) )
27	25 26	eleqtrd	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ ∈ ( ( Subcat ‘ 𝐶 ) ∩ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ) )
28	27	elin1d	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ ∈ ( Subcat ‘ 𝐶 ) )
29	28	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) → ℎ ∈ ( Subcat ‘ 𝐶 ) )
30	27	elin2d	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ ∈ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } )
31		vex	⊢ ℎ ∈ V
32		fneq1	⊢ ( 𝑗 = ℎ → ( 𝑗 Fn ( 𝑆 × 𝑆 ) ↔ ℎ Fn ( 𝑆 × 𝑆 ) ) )
33	31 32	elab	⊢ ( ℎ ∈ { 𝑗 ∣ 𝑗 Fn ( 𝑆 × 𝑆 ) } ↔ ℎ Fn ( 𝑆 × 𝑆 ) )
34	30 33	sylib	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ Fn ( 𝑆 × 𝑆 ) )
35	34	adantlr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) → ℎ Fn ( 𝑆 × 𝑆 ) )
36		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) → 𝑥 ∈ 𝑆 )
37	29 35 36 3	subcidcl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) )
38	37	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑥 ) )
39		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
40	39	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ℎ 𝑥 ) = ( 𝑥 ℎ 𝑦 ) )
41	38 40	eleqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( 𝑥 ℎ 𝑦 ) )
42	41	snssd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → { ( 𝐼 ‘ 𝑥 ) } ⊆ ( 𝑥 ℎ 𝑦 ) )
43		0ss	⊢ ∅ ⊆ ( 𝑥 ℎ 𝑦 )
44	43	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) ∧ ¬ 𝑥 = 𝑦 ) → ∅ ⊆ ( 𝑥 ℎ 𝑦 ) )
45	23 24 42 44	ifbothda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ ℎ ∈ 𝐴 ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ⊆ ( 𝑥 ℎ 𝑦 ) )
46	13 22 45	iinglb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∩ ℎ ∈ 𝐴 ( 𝑥 ℎ 𝑦 ) = if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) )
47	46	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) = ∩ ℎ ∈ 𝐴 ( 𝑥 ℎ 𝑦 ) )
48	11 12 47	mpoeq123dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ if ( 𝑥 = 𝑦 , { ( 𝐼 ‘ 𝑥 ) } , ∅ ) ) = ( 𝑥 ∈ ∩ ℎ ∈ 𝐴 𝑆 , 𝑦 ∈ ∩ ℎ ∈ 𝐴 𝑆 ↦ ∩ ℎ ∈ 𝐴 ( 𝑥 ℎ 𝑦 ) ) )
49	1 48	eqtrid	⊢ ( 𝜑 → 𝐽 = ( 𝑥 ∈ ∩ ℎ ∈ 𝐴 𝑆 , 𝑦 ∈ ∩ ℎ ∈ 𝐴 𝑆 ↦ ∩ ℎ ∈ 𝐴 ( 𝑥 ℎ 𝑦 ) ) )
50		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
51	28 50	subcssc	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → ℎ ⊆cat ( Homf ‘ 𝐶 ) )
52		eqidd	⊢ ( 𝜑 → ( 𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 ( ℎ ‘ 𝑧 ) ) = ( 𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 ( ℎ ‘ 𝑧 ) ) )
53		dmdm	⊢ ( ℎ Fn ( 𝑆 × 𝑆 ) → 𝑆 = dom dom ℎ )
54	34 53	syl	⊢ ( ( 𝜑 ∧ ℎ ∈ 𝐴 ) → 𝑆 = dom dom ℎ )
55		nfv	⊢ Ⅎ ℎ 𝜑
56	8 51 52 54 55	iinfssclem1	⊢ ( 𝜑 → ( 𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 ( ℎ ‘ 𝑧 ) ) = ( 𝑥 ∈ ∩ ℎ ∈ 𝐴 𝑆 , 𝑦 ∈ ∩ ℎ ∈ 𝐴 𝑆 ↦ ∩ ℎ ∈ 𝐴 ( 𝑥 ℎ 𝑦 ) ) )
57	49 56	eqtr4d	⊢ ( 𝜑 → 𝐽 = ( 𝑧 ∈ ∩ ℎ ∈ 𝐴 dom ℎ ↦ ∩ ℎ ∈ 𝐴 ( ℎ ‘ 𝑧 ) ) )