funcrngcsetcALT

Description: Alternate proof of funcrngcsetc , using cofuval2 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc , and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc . Surprisingly, this proof is longer than the direct proof given in funcrngcsetc . (Contributed by AV, 30-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcrngcsetcALT.r	$⊢ R = RngCat (U)$
	funcrngcsetcALT.s	$⊢ S = SetCat (U)$
	funcrngcsetcALT.b	$⊢ B = {Base}_{R}$
	funcrngcsetcALT.u	$⊢ φ \to U \in WUni$
	funcrngcsetcALT.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcrngcsetcALT.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RngHomo y)})$
Assertion	funcrngcsetcALT	$⊢ φ \to F (R Func S) G$

Proof

Step	Hyp	Ref	Expression
1		funcrngcsetcALT.r	$⊢ R = RngCat (U)$
2		funcrngcsetcALT.s	$⊢ S = SetCat (U)$
3		funcrngcsetcALT.b	$⊢ B = {Base}_{R}$
4		funcrngcsetcALT.u	$⊢ φ \to U \in WUni$
5		funcrngcsetcALT.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
6		funcrngcsetcALT.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RngHomo y)})$
7		fveq2	$⊢ x = u \to {Base}_{x} = {Base}_{u}$
8	7	cbvmptv	$⊢ (x \in B ⟼ {Base}_{x}) = (u \in B ⟼ {Base}_{u})$
9	5 8	eqtrdi	$⊢ φ \to F = (u \in B ⟼ {Base}_{u})$
10		coires1	$⊢ (u \in U ⟼ {Base}_{u}) \circ ({I ↾}_{B}) = {(u \in U ⟼ {Base}_{u}) ↾}_{B}$
11	1 3 4	rngcbas	$⊢ φ \to B = U \cap Rng$
12	11	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in (U \cap Rng))$
13		elin	$⊢ x \in (U \cap Rng) \leftrightarrow (x \in U \land x \in Rng)$
14	13	simplbi	$⊢ x \in (U \cap Rng) \to x \in U$
15	12 14	syl6bi	$⊢ φ \to (x \in B \to x \in U)$
16	15	ssrdv	$⊢ φ \to B \subseteq U$
17	16	resmptd	$⊢ φ \to {(u \in U ⟼ {Base}_{u}) ↾}_{B} = (u \in B ⟼ {Base}_{u})$
18	10 17	eqtr2id	$⊢ φ \to (u \in B ⟼ {Base}_{u}) = (u \in U ⟼ {Base}_{u}) \circ ({I ↾}_{B})$
19	9 18	eqtrd	$⊢ φ \to F = (u \in U ⟼ {Base}_{u}) \circ ({I ↾}_{B})$
20		coires1	$⊢ ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)}) = {({I ↾}_{({Base}_{y}^{{Base}_{x}})}) ↾}_{(x RngHomo y)}$
21		eqid	$⊢ {Base}_{x} = {Base}_{x}$
22		eqid	$⊢ {Base}_{y} = {Base}_{y}$
23	21 22	rnghmf	$⊢ z \in (x RngHomo y) \to z : {Base}_{x} ⟶ {Base}_{y}$
24		fvex	$⊢ {Base}_{y} \in V$
25		fvex	$⊢ {Base}_{x} \in V$
26	24 25	pm3.2i	$⊢ ({Base}_{y} \in V \land {Base}_{x} \in V)$
27		elmapg	$⊢ ({Base}_{y} \in V \land {Base}_{x} \in V) \to (z \in ({Base}_{y}^{{Base}_{x}}) \leftrightarrow z : {Base}_{x} ⟶ {Base}_{y})$
28	26 27	mp1i	$⊢ (φ \land x \in B \land y \in B) \to (z \in ({Base}_{y}^{{Base}_{x}}) \leftrightarrow z : {Base}_{x} ⟶ {Base}_{y})$
29	23 28	syl5ibr	$⊢ (φ \land x \in B \land y \in B) \to (z \in (x RngHomo y) \to z \in ({Base}_{y}^{{Base}_{x}}))$
30	29	ssrdv	$⊢ (φ \land x \in B \land y \in B) \to x RngHomo y \subseteq {Base}_{y}^{{Base}_{x}}$
31	30	resabs1d	$⊢ (φ \land x \in B \land y \in B) \to {({I ↾}_{({Base}_{y}^{{Base}_{x}})}) ↾}_{(x RngHomo y)} = {I ↾}_{(x RngHomo y)}$
32	20 31	eqtr2id	$⊢ (φ \land x \in B \land y \in B) \to {I ↾}_{(x RngHomo y)} = ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)})$
33	32	mpoeq3dva	$⊢ φ \to (x \in B, y \in B ⟼ {I ↾}_{(x RngHomo y)}) = (x \in B, y \in B ⟼ ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)}))$
34	6 33	eqtrd	$⊢ φ \to G = (x \in B, y \in B ⟼ ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)}))$
35	3	a1i	$⊢ φ \to B = {Base}_{R}$
36	3	a1i	$⊢ (φ \land x \in B) \to B = {Base}_{R}$
37		fvresi	$⊢ x \in B \to ({I ↾}_{B}) (x) = x$
38	37	adantr	$⊢ (x \in B \land y \in B) \to ({I ↾}_{B}) (x) = x$
39	38	adantl	$⊢ (φ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) = x$
40		fvresi	$⊢ y \in B \to ({I ↾}_{B}) (y) = y$
41	40	adantl	$⊢ (x \in B \land y \in B) \to ({I ↾}_{B}) (y) = y$
42	41	adantl	$⊢ (φ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (y) = y$
43	39 42	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to ({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y) = x (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) y$
44		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) = (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})$
45		simprr	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to z = y$
46	45	fveq2d	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to {Base}_{z} = {Base}_{y}$
47		simprl	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to w = x$
48	47	fveq2d	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to {Base}_{w} = {Base}_{x}$
49	46 48	oveq12d	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to {Base}_{z}^{{Base}_{w}} = {Base}_{y}^{{Base}_{x}}$
50	49	reseq2d	$⊢ ((φ \land (x \in B \land y \in B)) \land (w = x \land z = y)) \to {I ↾}_{({Base}_{z}^{{Base}_{w}})} = {I ↾}_{({Base}_{y}^{{Base}_{x}})}$
51	15	com12	$⊢ x \in B \to (φ \to x \in U)$
52	51	adantr	$⊢ (x \in B \land y \in B) \to (φ \to x \in U)$
53	52	impcom	$⊢ (φ \land (x \in B \land y \in B)) \to x \in U$
54	11	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in (U \cap Rng))$
55		elin	$⊢ y \in (U \cap Rng) \leftrightarrow (y \in U \land y \in Rng)$
56	55	simplbi	$⊢ y \in (U \cap Rng) \to y \in U$
57	54 56	syl6bi	$⊢ φ \to (y \in B \to y \in U)$
58	57	a1d	$⊢ φ \to (x \in B \to (y \in B \to y \in U))$
59	58	imp32	$⊢ (φ \land (x \in B \land y \in B)) \to y \in U$
60		ovex	$⊢ {Base}_{y}^{{Base}_{x}} \in V$
61	60	a1i	$⊢ (φ \land (x \in B \land y \in B)) \to {Base}_{y}^{{Base}_{x}} \in V$
62	61	resiexd	$⊢ (φ \land (x \in B \land y \in B)) \to {I ↾}_{({Base}_{y}^{{Base}_{x}})} \in V$
63	44 50 53 59 62	ovmpod	$⊢ (φ \land (x \in B \land y \in B)) \to x (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) y = {I ↾}_{({Base}_{y}^{{Base}_{x}})}$
64	43 63	eqtr2d	$⊢ (φ \land (x \in B \land y \in B)) \to {I ↾}_{({Base}_{y}^{{Base}_{x}})} = ({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)$
65		eqidd	$⊢ (φ \land (x \in B \land y \in B)) \to (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) = (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})$
66		oveq12	$⊢ (f = x \land g = y) \to f RngHomo g = x RngHomo y$
67	66	reseq2d	$⊢ (f = x \land g = y) \to {I ↾}_{(f RngHomo g)} = {I ↾}_{(x RngHomo y)}$
68	67	adantl	$⊢ ((φ \land (x \in B \land y \in B)) \land (f = x \land g = y)) \to {I ↾}_{(f RngHomo g)} = {I ↾}_{(x RngHomo y)}$
69		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
70		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
71		ovex	$⊢ x RngHomo y \in V$
72	71	a1i	$⊢ (φ \land (x \in B \land y \in B)) \to x RngHomo y \in V$
73	72	resiexd	$⊢ (φ \land (x \in B \land y \in B)) \to {I ↾}_{(x RngHomo y)} \in V$
74	65 68 69 70 73	ovmpod	$⊢ (φ \land (x \in B \land y \in B)) \to x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y = {I ↾}_{(x RngHomo y)}$
75	74	eqcomd	$⊢ (φ \land (x \in B \land y \in B)) \to {I ↾}_{(x RngHomo y)} = x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y$
76	64 75	coeq12d	$⊢ (φ \land (x \in B \land y \in B)) \to ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)}) = (({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)) \circ (x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y)$
77	35 36 76	mpoeq123dva	$⊢ φ \to (x \in B, y \in B ⟼ ({I ↾}_{({Base}_{y}^{{Base}_{x}})}) \circ ({I ↾}_{(x RngHomo y)})) = (x \in {Base}_{R}, y \in {Base}_{R} ⟼ (({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)) \circ (x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y))$
78	34 77	eqtrd	$⊢ φ \to G = (x \in {Base}_{R}, y \in {Base}_{R} ⟼ (({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)) \circ (x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y))$
79	19 78	opeq12d	$⊢ φ \to ⟨F, G⟩ = ⟨(u \in U ⟼ {Base}_{u}) \circ ({I ↾}_{B}), (x \in {Base}_{R}, y \in {Base}_{R} ⟼ (({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)) \circ (x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y))⟩$
80		eqid	$⊢ {Base}_{R} = {Base}_{R}$
81		eqid	$⊢ ExtStrCat (U) = ExtStrCat (U)$
82		eqidd	$⊢ φ \to {I ↾}_{B} = {I ↾}_{B}$
83		eqidd	$⊢ φ \to (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) = (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})$
84	1 81 3 4 82 83	rngcifuestrc	$⊢ φ \to ({I ↾}_{B}) (R Func ExtStrCat (U)) (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})$
85		eqid	$⊢ {Base}_{ExtStrCat (U)} = {Base}_{ExtStrCat (U)}$
86		eqid	$⊢ {Base}_{S} = {Base}_{S}$
87	81 4	estrcbas	$⊢ φ \to U = {Base}_{ExtStrCat (U)}$
88	87	mpteq1d	$⊢ φ \to (u \in U ⟼ {Base}_{u}) = (u \in {Base}_{ExtStrCat (U)} ⟼ {Base}_{u})$
89		fveq2	$⊢ w = u \to {Base}_{w} = {Base}_{u}$
90	89	oveq2d	$⊢ w = u \to {Base}_{z}^{{Base}_{w}} = {Base}_{z}^{{Base}_{u}}$
91	90	reseq2d	$⊢ w = u \to {I ↾}_{({Base}_{z}^{{Base}_{w}})} = {I ↾}_{({Base}_{z}^{{Base}_{u}})}$
92		fveq2	$⊢ z = v \to {Base}_{z} = {Base}_{v}$
93	92	oveq1d	$⊢ z = v \to {Base}_{z}^{{Base}_{u}} = {Base}_{v}^{{Base}_{u}}$
94	93	reseq2d	$⊢ z = v \to {I ↾}_{({Base}_{z}^{{Base}_{u}})} = {I ↾}_{({Base}_{v}^{{Base}_{u}})}$
95	91 94	cbvmpov	$⊢ (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) = (u \in U, v \in U ⟼ {I ↾}_{({Base}_{v}^{{Base}_{u}})})$
96	95	a1i	$⊢ φ \to (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) = (u \in U, v \in U ⟼ {I ↾}_{({Base}_{v}^{{Base}_{u}})})$
97		eqidd	$⊢ φ \to {I ↾}_{({Base}_{v}^{{Base}_{u}})} = {I ↾}_{({Base}_{v}^{{Base}_{u}})}$
98	87 87 97	mpoeq123dv	$⊢ φ \to (u \in U, v \in U ⟼ {I ↾}_{({Base}_{v}^{{Base}_{u}})}) = (u \in {Base}_{ExtStrCat (U)}, v \in {Base}_{ExtStrCat (U)} ⟼ {I ↾}_{({Base}_{v}^{{Base}_{u}})})$
99	96 98	eqtrd	$⊢ φ \to (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) = (u \in {Base}_{ExtStrCat (U)}, v \in {Base}_{ExtStrCat (U)} ⟼ {I ↾}_{({Base}_{v}^{{Base}_{u}})})$
100	81 2 85 86 4 88 99	funcestrcsetc	$⊢ φ \to (u \in U ⟼ {Base}_{u}) (ExtStrCat (U) Func S) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})$
101	80 84 100	cofuval2	$⊢ φ \to ⟨(u \in U ⟼ {Base}_{u}), (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})⟩ \circ_{func} ⟨{I ↾}_{B}, (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})⟩ = ⟨(u \in U ⟼ {Base}_{u}) \circ ({I ↾}_{B}), (x \in {Base}_{R}, y \in {Base}_{R} ⟼ (({I ↾}_{B}) (x) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) ({I ↾}_{B}) (y)) \circ (x (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) y))⟩$
102	79 101	eqtr4d	$⊢ φ \to ⟨F, G⟩ = ⟨(u \in U ⟼ {Base}_{u}), (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})⟩ \circ_{func} ⟨{I ↾}_{B}, (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})⟩$
103		df-br	$⊢ ({I ↾}_{B}) (R Func ExtStrCat (U)) (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)}) \leftrightarrow ⟨{I ↾}_{B}, (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})⟩ \in (R Func ExtStrCat (U))$
104	84 103	sylib	$⊢ φ \to ⟨{I ↾}_{B}, (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})⟩ \in (R Func ExtStrCat (U))$
105		df-br	$⊢ (u \in U ⟼ {Base}_{u}) (ExtStrCat (U) Func S) (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})}) \leftrightarrow ⟨(u \in U ⟼ {Base}_{u}), (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})⟩ \in (ExtStrCat (U) Func S)$
106	100 105	sylib	$⊢ φ \to ⟨(u \in U ⟼ {Base}_{u}), (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})⟩ \in (ExtStrCat (U) Func S)$
107	104 106	cofucl	$⊢ φ \to ⟨(u \in U ⟼ {Base}_{u}), (w \in U, z \in U ⟼ {I ↾}_{({Base}_{z}^{{Base}_{w}})})⟩ \circ_{func} ⟨{I ↾}_{B}, (f \in B, g \in B ⟼ {I ↾}_{(f RngHomo g)})⟩ \in (R Func S)$
108	102 107	eqeltrd	$⊢ φ \to ⟨F, G⟩ \in (R Func S)$
109		df-br	$⊢ F (R Func S) G \leftrightarrow ⟨F, G⟩ \in (R Func S)$
110	108 109	sylibr	$⊢ φ \to F (R Func S) G$

Metamath Proof Explorer

Theorem funcrngcsetcALT

Proof