Metamath Proof Explorer

Theorem rngccatidALTV

Description: Lemma for rngccatALTV . (New usage is discouraged.) (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses rngccatALTV.c 
|- C = ( RngCatALTV ` U )
rngccatidALTV.b 
|- B = ( Base ` C )
Assertion rngccatidALTV 
|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rngccatALTV.c 
 |-  C = ( RngCatALTV ` U )
2 rngccatidALTV.b 
 |-  B = ( Base ` C )
3 2 a1i 
 |-  ( U e. V -> B = ( Base ` C ) )
4 eqidd 
 |-  ( U e. V -> ( Hom ` C ) = ( Hom ` C ) )
5 eqidd 
 |-  ( U e. V -> ( comp ` C ) = ( comp ` C ) )
6 1 fvexi 
 |-  C e. _V
7 6 a1i 
 |-  ( U e. V -> C e. _V )
8 biid 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) <-> ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) )
9 simpl 
 |-  ( ( U e. V /\ x e. B ) -> U e. V )
10 1 2 9 rngcbasALTV 
 |-  ( ( U e. V /\ x e. B ) -> B = ( U i^i Rng ) )
11 eleq2 
 |-  ( B = ( U i^i Rng ) -> ( x e. B <-> x e. ( U i^i Rng ) ) )
12 elin 
 |-  ( x e. ( U i^i Rng ) <-> ( x e. U /\ x e. Rng ) )
13 12 simprbi 
 |-  ( x e. ( U i^i Rng ) -> x e. Rng )
14 11 13 syl6bi 
 |-  ( B = ( U i^i Rng ) -> ( x e. B -> x e. Rng ) )
15 14 com12 
 |-  ( x e. B -> ( B = ( U i^i Rng ) -> x e. Rng ) )
16 15 adantl 
 |-  ( ( U e. V /\ x e. B ) -> ( B = ( U i^i Rng ) -> x e. Rng ) )
17 10 16 mpd 
 |-  ( ( U e. V /\ x e. B ) -> x e. Rng )
18 eqid 
 |-  ( Base ` x ) = ( Base ` x )
19 18 idrnghm 
 |-  ( x e. Rng -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) )
20 17 19 syl 
 |-  ( ( U e. V /\ x e. B ) -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) )
21 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
22 simpr 
 |-  ( ( U e. V /\ x e. B ) -> x e. B )
23 1 2 9 21 22 22 rngchomALTV 
 |-  ( ( U e. V /\ x e. B ) -> ( x ( Hom ` C ) x ) = ( x RngHomo x ) )
24 20 23 eleqtrrd 
 |-  ( ( U e. V /\ x e. B ) -> ( _I |` ( Base ` x ) ) e. ( x ( Hom ` C ) x ) )
25 simpl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> U e. V )
26 eqid 
 |-  ( comp ` C ) = ( comp ` C )
27 simpl 
 |-  ( ( w e. B /\ x e. B ) -> w e. B )
28 27 3ad2ant1 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> w e. B )
29 28 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> w e. B )
30 simpr 
 |-  ( ( w e. B /\ x e. B ) -> x e. B )
31 30 3ad2ant1 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> x e. B )
32 31 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> x e. B )
33 simp1 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> U e. V )
34 27 3ad2ant3 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> w e. B )
35 30 3ad2ant3 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> x e. B )
36 1 2 33 21 34 35 rngchomALTV 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( w ( Hom ` C ) x ) = ( w RngHomo x ) )
37 36 eleq2d 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( f e. ( w ( Hom ` C ) x ) <-> f e. ( w RngHomo x ) ) )
38 37 biimpd 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( f e. ( w ( Hom ` C ) x ) -> f e. ( w RngHomo x ) ) )
39 38 3exp 
 |-  ( U e. V -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( f e. ( w ( Hom ` C ) x ) -> f e. ( w RngHomo x ) ) ) ) )
40 39 com14 
 |-  ( f e. ( w ( Hom ` C ) x ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> f e. ( w RngHomo x ) ) ) ) )
41 40 3ad2ant1 
 |-  ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> f e. ( w RngHomo x ) ) ) ) )
42 41 com13 
 |-  ( ( w e. B /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> f e. ( w RngHomo x ) ) ) ) )
43 42 3imp 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> f e. ( w RngHomo x ) ) )
44 43 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> f e. ( w RngHomo x ) )
45 20 expcom 
 |-  ( x e. B -> ( U e. V -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) ) )
46 45 adantl 
 |-  ( ( w e. B /\ x e. B ) -> ( U e. V -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) ) )
47 46 3ad2ant1 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) ) )
48 47 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) )
49 1 2 25 26 29 32 32 44 48 rngccoALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` ( Base ` x ) ) ( <. w , x >. ( comp ` C ) x ) f ) = ( ( _I |` ( Base ` x ) ) o. f ) )
50 simpl 
 |-  ( ( U e. V /\ ( w e. B /\ x e. B ) ) -> U e. V )
51 simprl 
 |-  ( ( U e. V /\ ( w e. B /\ x e. B ) ) -> w e. B )
52 simprr 
 |-  ( ( U e. V /\ ( w e. B /\ x e. B ) ) -> x e. B )
53 1 2 50 21 51 52 elrngchomALTV 
 |-  ( ( U e. V /\ ( w e. B /\ x e. B ) ) -> ( f e. ( w ( Hom ` C ) x ) -> f : ( Base ` w ) --> ( Base ` x ) ) )
54 53 ex 
 |-  ( U e. V -> ( ( w e. B /\ x e. B ) -> ( f e. ( w ( Hom ` C ) x ) -> f : ( Base ` w ) --> ( Base ` x ) ) ) )
55 54 com13 
 |-  ( f e. ( w ( Hom ` C ) x ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> f : ( Base ` w ) --> ( Base ` x ) ) ) )
56 fcoi2 
 |-  ( f : ( Base ` w ) --> ( Base ` x ) -> ( ( _I |` ( Base ` x ) ) o. f ) = f )
57 55 56 syl8 
 |-  ( f e. ( w ( Hom ` C ) x ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> ( ( _I |` ( Base ` x ) ) o. f ) = f ) ) )
58 57 3ad2ant1 
 |-  ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> ( ( _I |` ( Base ` x ) ) o. f ) = f ) ) )
59 58 com12 
 |-  ( ( w e. B /\ x e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> ( ( _I |` ( Base ` x ) ) o. f ) = f ) ) )
60 59 a1d 
 |-  ( ( w e. B /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> ( ( _I |` ( Base ` x ) ) o. f ) = f ) ) ) )
61 60 3imp 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> ( ( _I |` ( Base ` x ) ) o. f ) = f ) )
62 61 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` ( Base ` x ) ) o. f ) = f )
63 49 62 eqtrd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( _I |` ( Base ` x ) ) ( <. w , x >. ( comp ` C ) x ) f ) = f )
64 simp3 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> U e. V )
65 30 adantr 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> x e. B )
66 65 3ad2ant2 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> x e. B )
67 simprl 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> y e. B )
68 67 3ad2ant2 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> y e. B )
69 46 adantr 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) ) )
70 69 a1i 
 |-  ( g e. ( x ( Hom ` C ) y ) -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) ) ) )
71 70 3imp 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> ( _I |` ( Base ` x ) ) e. ( x RngHomo x ) )
72 simpl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> U e. V )
73 65 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> x e. B )
74 67 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> y e. B )
75 1 2 72 21 73 74 rngchomALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> ( x ( Hom ` C ) y ) = ( x RngHomo y ) )
76 75 eleq2d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> ( g e. ( x ( Hom ` C ) y ) <-> g e. ( x RngHomo y ) ) )
77 76 biimpd 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> ( g e. ( x ( Hom ` C ) y ) -> g e. ( x RngHomo y ) ) )
78 77 ex 
 |-  ( U e. V -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( g e. ( x ( Hom ` C ) y ) -> g e. ( x RngHomo y ) ) ) )
79 78 com13 
 |-  ( g e. ( x ( Hom ` C ) y ) -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> g e. ( x RngHomo y ) ) ) )
80 79 3imp 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> g e. ( x RngHomo y ) )
81 1 2 64 26 66 66 68 71 80 rngccoALTV 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = ( g o. ( _I |` ( Base ` x ) ) ) )
82 1 2 72 21 73 74 elrngchomALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) ) -> ( g e. ( x ( Hom ` C ) y ) -> g : ( Base ` x ) --> ( Base ` y ) ) )
83 82 ex 
 |-  ( U e. V -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( g e. ( x ( Hom ` C ) y ) -> g : ( Base ` x ) --> ( Base ` y ) ) ) )
84 83 com13 
 |-  ( g e. ( x ( Hom ` C ) y ) -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> g : ( Base ` x ) --> ( Base ` y ) ) ) )
85 84 3imp 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> g : ( Base ` x ) --> ( Base ` y ) )
86 fcoi1 
 |-  ( g : ( Base ` x ) --> ( Base ` y ) -> ( g o. ( _I |` ( Base ` x ) ) ) = g )
87 85 86 syl 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> ( g o. ( _I |` ( Base ` x ) ) ) = g )
88 81 87 eqtrd 
 |-  ( ( g e. ( x ( Hom ` C ) y ) /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) /\ U e. V ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g )
89 88 3exp 
 |-  ( g e. ( x ( Hom ` C ) y ) -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g ) ) )
90 89 3ad2ant2 
 |-  ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) ) -> ( U e. V -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g ) ) )
91 90 expdcom 
 |-  ( ( w e. B /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g ) ) ) )
92 91 3imp 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g ) )
93 92 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. x , x >. ( comp ` C ) y ) ( _I |` ( Base ` x ) ) ) = g )
94 simp2l 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> y e. B )
95 1 2 33 21 35 94 rngchomALTV 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( x ( Hom ` C ) y ) = ( x RngHomo y ) )
96 95 eleq2d 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( g e. ( x ( Hom ` C ) y ) <-> g e. ( x RngHomo y ) ) )
97 96 biimpd 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( g e. ( x ( Hom ` C ) y ) -> g e. ( x RngHomo y ) ) )
98 97 3exp 
 |-  ( U e. V -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( g e. ( x ( Hom ` C ) y ) -> g e. ( x RngHomo y ) ) ) ) )
99 98 com14 
 |-  ( g e. ( x ( Hom ` C ) y ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> g e. ( x RngHomo y ) ) ) ) )
100 99 3ad2ant2 
 |-  ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> g e. ( x RngHomo y ) ) ) ) )
101 100 com13 
 |-  ( ( w e. B /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> g e. ( x RngHomo y ) ) ) ) )
102 101 3imp 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> g e. ( x RngHomo y ) ) )
103 102 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> g e. ( x RngHomo y ) )
104 rnghmco 
 |-  ( ( g e. ( x RngHomo y ) /\ f e. ( w RngHomo x ) ) -> ( g o. f ) e. ( w RngHomo y ) )
105 103 44 104 syl2anc 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g o. f ) e. ( w RngHomo y ) )
106 simp2l 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> y e. B )
107 106 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> y e. B )
108 1 2 25 26 29 32 107 44 103 rngccoALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. w , x >. ( comp ` C ) y ) f ) = ( g o. f ) )
109 1 2 25 21 29 107 rngchomALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( w ( Hom ` C ) y ) = ( w RngHomo y ) )
110 105 108 109 3eltr4d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( g ( <. w , x >. ( comp ` C ) y ) f ) e. ( w ( Hom ` C ) y ) )
111 coass 
 |-  ( ( h o. g ) o. f ) = ( h o. ( g o. f ) )
112 simp2r 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> z e. B )
113 112 adantl 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> z e. B )
114 simp2r 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> z e. B )
115 1 2 33 21 94 114 rngchomALTV 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( y ( Hom ` C ) z ) = ( y RngHomo z ) )
116 115 eleq2d 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( h e. ( y ( Hom ` C ) z ) <-> h e. ( y RngHomo z ) ) )
117 116 biimpd 
 |-  ( ( U e. V /\ ( y e. B /\ z e. B ) /\ ( w e. B /\ x e. B ) ) -> ( h e. ( y ( Hom ` C ) z ) -> h e. ( y RngHomo z ) ) )
118 117 3exp 
 |-  ( U e. V -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( h e. ( y ( Hom ` C ) z ) -> h e. ( y RngHomo z ) ) ) ) )
119 118 com14 
 |-  ( h e. ( y ( Hom ` C ) z ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> h e. ( y RngHomo z ) ) ) ) )
120 119 3ad2ant3 
 |-  ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( ( y e. B /\ z e. B ) -> ( ( w e. B /\ x e. B ) -> ( U e. V -> h e. ( y RngHomo z ) ) ) ) )
121 120 com13 
 |-  ( ( w e. B /\ x e. B ) -> ( ( y e. B /\ z e. B ) -> ( ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) -> ( U e. V -> h e. ( y RngHomo z ) ) ) ) )
122 121 3imp 
 |-  ( ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) -> ( U e. V -> h e. ( y RngHomo z ) ) )
123 122 impcom 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> h e. ( y RngHomo z ) )
124 rnghmco 
 |-  ( ( h e. ( y RngHomo z ) /\ g e. ( x RngHomo y ) ) -> ( h o. g ) e. ( x RngHomo z ) )
125 123 103 124 syl2anc 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h o. g ) e. ( x RngHomo z ) )
126 1 2 25 26 29 32 113 44 125 rngccoALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( ( h o. g ) o. f ) )
127 1 2 25 26 29 107 113 105 123 rngccoALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) = ( h o. ( g o. f ) ) )
128 111 126 127 3eqtr4a 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) )
129 1 2 25 26 32 107 113 103 123 rngccoALTV 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. x , y >. ( comp ` C ) z ) g ) = ( h o. g ) )
130 129 oveq1d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h ( <. x , y >. ( comp ` C ) z ) g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( ( h o. g ) ( <. w , x >. ( comp ` C ) z ) f ) )
131 108 oveq2d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( h ( <. w , y >. ( comp ` C ) z ) ( g ( <. w , x >. ( comp ` C ) y ) f ) ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g o. f ) ) )
132 128 130 131 3eqtr4d 
 |-  ( ( U e. V /\ ( ( w e. B /\ x e. B ) /\ ( y e. B /\ z e. B ) /\ ( f e. ( w ( Hom ` C ) x ) /\ g e. ( x ( Hom ` C ) y ) /\ h e. ( y ( Hom ` C ) z ) ) ) ) -> ( ( h ( <. x , y >. ( comp ` C ) z ) g ) ( <. w , x >. ( comp ` C ) z ) f ) = ( h ( <. w , y >. ( comp ` C ) z ) ( g ( <. w , x >. ( comp ` C ) y ) f ) ) )
133 3 4 5 7 8 24 63 93 110 132 iscatd2 
 |-  ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )