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

Metamath Proof Explorer

Theorem rngccatidALTV

Proof