Metamath Proof Explorer

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 
|- 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 iinfconstbas 
|- ( ph -> J = ( z e. |^|_ h e. A dom h |-> |^|_ h e. A ( h ` z ) ) )

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 6 iinfconstbaslem 
 |-  ( ph -> J e. A )
8 7 ne0d 
 |-  ( ph -> A =/= (/) )
9 iinconst 
 |-  ( A =/= (/) -> |^|_ h e. A S = S )
10 8 9 syl 
 |-  ( ph -> |^|_ h e. A S = S )
11 10 eqcomd 
 |-  ( ph -> S = |^|_ h e. A S )
12 11 adantr 
 |-  ( ( ph /\ x e. S ) -> S = |^|_ h e. A S )
13 7 adantr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> J e. A )
14 simpr 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h = J ) -> h = J )
15 14 oveqd 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h = J ) -> ( x h y ) = ( x J y ) )
16 snex 
 |-  { ( I ` x ) } e. _V
17 0ex 
 |-  (/) e. _V
18 16 17 ifex 
 |-  if ( x = y , { ( I ` x ) } , (/) ) e. _V
19 1 ovmpt4g 
 |-  ( ( x e. S /\ y e. S /\ if ( x = y , { ( I ` x ) } , (/) ) e. _V ) -> ( x J y ) = if ( x = y , { ( I ` x ) } , (/) ) )
20 18 19 mp3an3 
 |-  ( ( x e. S /\ y e. S ) -> ( x J y ) = if ( x = y , { ( I ` x ) } , (/) ) )
21 20 ad2antlr 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h = J ) -> ( x J y ) = if ( x = y , { ( I ` x ) } , (/) ) )
22 15 21 eqtrd 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h = J ) -> ( x h y ) = if ( x = y , { ( I ` x ) } , (/) ) )
23 sseq1 
 |-  ( { ( I ` x ) } = if ( x = y , { ( I ` x ) } , (/) ) -> ( { ( I ` x ) } C_ ( x h y ) <-> if ( x = y , { ( I ` x ) } , (/) ) C_ ( x h y ) ) )
24 sseq1 
 |-  ( (/) = if ( x = y , { ( I ` x ) } , (/) ) -> ( (/) C_ ( x h y ) <-> if ( x = y , { ( I ` x ) } , (/) ) C_ ( x h y ) ) )
25 simpr 
 |-  ( ( ph /\ h e. A ) -> h e. A )
26 6 adantr 
 |-  ( ( ph /\ h e. A ) -> A = ( ( Subcat ` C ) i^i { j | j Fn ( S X. S ) } ) )
27 25 26 eleqtrd 
 |-  ( ( ph /\ h e. A ) -> h e. ( ( Subcat ` C ) i^i { j | j Fn ( S X. S ) } ) )
28 27 elin1d 
 |-  ( ( ph /\ h e. A ) -> h e. ( Subcat ` C ) )
29 28 adantlr 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) -> h e. ( Subcat ` C ) )
30 27 elin2d 
 |-  ( ( ph /\ h e. A ) -> h e. { j | j Fn ( S X. S ) } )
31 vex 
 |-  h e. _V
32 fneq1 
 |-  ( j = h -> ( j Fn ( S X. S ) <-> h Fn ( S X. S ) ) )
33 31 32 elab 
 |-  ( h e. { j | j Fn ( S X. S ) } <-> h Fn ( S X. S ) )
34 30 33 sylib 
 |-  ( ( ph /\ h e. A ) -> h Fn ( S X. S ) )
35 34 adantlr 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) -> h Fn ( S X. S ) )
36 simplrl 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) -> x e. S )
37 29 35 36 3 subcidcl 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) -> ( I ` x ) e. ( x h x ) )
38 37 adantr 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ x = y ) -> ( I ` x ) e. ( x h x ) )
39 simpr 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ x = y ) -> x = y )
40 39 oveq2d 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ x = y ) -> ( x h x ) = ( x h y ) )
41 38 40 eleqtrd 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ x = y ) -> ( I ` x ) e. ( x h y ) )
42 41 snssd 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ x = y ) -> { ( I ` x ) } C_ ( x h y ) )
43 0ss 
 |-  (/) C_ ( x h y )
44 43 a1i 
 |-  ( ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) /\ -. x = y ) -> (/) C_ ( x h y ) )
45 23 24 42 44 ifbothda 
 |-  ( ( ( ph /\ ( x e. S /\ y e. S ) ) /\ h e. A ) -> if ( x = y , { ( I ` x ) } , (/) ) C_ ( x h y ) )
46 13 22 45 iinglb 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> |^|_ h e. A ( x h y ) = if ( x = y , { ( I ` x ) } , (/) ) )
47 46 eqcomd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> if ( x = y , { ( I ` x ) } , (/) ) = |^|_ h e. A ( x h y ) )
48 11 12 47 mpoeq123dva 
 |-  ( ph -> ( x e. S , y e. S |-> if ( x = y , { ( I ` x ) } , (/) ) ) = ( x e. |^|_ h e. A S , y e. |^|_ h e. A S |-> |^|_ h e. A ( x h y ) ) )
49 1 48 eqtrid 
 |-  ( ph -> J = ( x e. |^|_ h e. A S , y e. |^|_ h e. A S |-> |^|_ h e. A ( x h y ) ) )
50 eqid 
 |-  ( Homf ` C ) = ( Homf ` C )
51 28 50 subcssc 
 |-  ( ( ph /\ h e. A ) -> h C_cat ( Homf ` C ) )
52 eqidd 
 |-  ( ph -> ( z e. |^|_ h e. A dom h |-> |^|_ h e. A ( h ` z ) ) = ( z e. |^|_ h e. A dom h |-> |^|_ h e. A ( h ` z ) ) )
53 dmdm 
 |-  ( h Fn ( S X. S ) -> S = dom dom h )
54 34 53 syl 
 |-  ( ( ph /\ h e. A ) -> S = dom dom h )
55 nfv 
 |-  F/ h ph
56 8 51 52 54 55 iinfssclem1 
 |-  ( ph -> ( z e. |^|_ h e. A dom h |-> |^|_ h e. A ( h ` z ) ) = ( x e. |^|_ h e. A S , y e. |^|_ h e. A S |-> |^|_ h e. A ( x h y ) ) )
57 49 56 eqtr4d 
 |-  ( ph -> J = ( z e. |^|_ h e. A dom h |-> |^|_ h e. A ( h ` z ) ) )