Theorem funcrngcsetcALT 20550

Description: Alternate proof of funcrngcsetc 20549, using cofuval2 17849 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 20548, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 18110. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 20549. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
funcrngcsetcALT.r	⊢ 𝑅 = (RngCat‘𝑈)
funcrngcsetcALT.s	⊢ 𝑆 = (SetCat‘𝑈)
funcrngcsetcALT.b	⊢ 𝐵 = (Base‘𝑅)
funcrngcsetcALT.u	⊢ (𝜑 → 𝑈 ∈ WUni)
funcrngcsetcALT.f	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))
funcrngcsetcALT.g	⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))

Assertion

Ref	Expression
funcrngcsetcALT	⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)

Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦   𝜑,𝑥,𝑦

Allowed substitution hints:   𝑆(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem funcrngcsetcALT

Dummy variables 𝑓 𝑔 𝑢 𝑤 𝑧 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funcrngcsetcALT.f	. . . . . . 7 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)))
2		fveq2 6858	. . . . . . . 8 ⊢ (𝑥 = 𝑢 → (Base‘𝑥) = (Base‘𝑢))
3	2	cbvmptv 5211	. . . . . . 7 ⊢ (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)) = (𝑢 ∈ 𝐵 ↦ (Base‘𝑢))
4	1, 3	eqtrdi 2780	. . . . . 6 ⊢ (𝜑 → 𝐹 = (𝑢 ∈ 𝐵 ↦ (Base‘𝑢)))
5		coires1 6237	. . . . . . 7 ⊢ ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)) = ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ↾ 𝐵)
6		funcrngcsetcALT.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (RngCat‘𝑈)
7		funcrngcsetcALT.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑅)
8		funcrngcsetcALT.u	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ WUni)
9	6, 7, 8	rngcbas 20530	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 = (𝑈 ∩ Rng))
10	9	eleq2d 2814	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ (𝑈 ∩ Rng)))
11		elin 3930	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝑈 ∩ Rng) ↔ (𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng))
12	11	simplbi 497	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝑈 ∩ Rng) → 𝑥 ∈ 𝑈)
13	10, 12	biimtrdi 253	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈))
14	13	ssrdv 3952	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ⊆ 𝑈)
15	14	resmptd 6011	. . . . . . 7 ⊢ (𝜑 → ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ↾ 𝐵) = (𝑢 ∈ 𝐵 ↦ (Base‘𝑢)))
16	5, 15	eqtr2id 2777	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝐵 ↦ (Base‘𝑢)) = ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)))
17	4, 16	eqtrd 2764	. . . . 5 ⊢ (𝜑 → 𝐹 = ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)))
18		funcrngcsetcALT.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))))
19		coires1 6237	. . . . . . . . 9 ⊢ (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦))) = (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ↾ (𝑥 RngHom 𝑦))
20		eqid 2729	. . . . . . . . . . . . 13 ⊢ (Base‘𝑥) = (Base‘𝑥)
21		eqid 2729	. . . . . . . . . . . . 13 ⊢ (Base‘𝑦) = (Base‘𝑦)
22	20, 21	rnghmf 20357	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ (𝑥 RngHom 𝑦) → 𝑧:(Base‘𝑥)⟶(Base‘𝑦))
23		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑦) ∈ V
24		fvex 6871	. . . . . . . . . . . . . 14 ⊢ (Base‘𝑥) ∈ V
25	23, 24	pm3.2i 470	. . . . . . . . . . . . 13 ⊢ ((Base‘𝑦) ∈ V ∧ (Base‘𝑥) ∈ V)
26		elmapg 8812	. . . . . . . . . . . . 13 ⊢ (((Base‘𝑦) ∈ V ∧ (Base‘𝑥) ∈ V) → (𝑧 ∈ ((Base‘𝑦) ↑m (Base‘𝑥)) ↔ 𝑧:(Base‘𝑥)⟶(Base‘𝑦)))
27	25, 26	mp1i 13	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ ((Base‘𝑦) ↑m (Base‘𝑥)) ↔ 𝑧:(Base‘𝑥)⟶(Base‘𝑦)))
28	22, 27	imbitrrid 246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ (𝑥 RngHom 𝑦) → 𝑧 ∈ ((Base‘𝑦) ↑m (Base‘𝑥))))
29	28	ssrdv 3952	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 RngHom 𝑦) ⊆ ((Base‘𝑦) ↑m (Base‘𝑥)))
30	29	resabs1d 5979	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ↾ (𝑥 RngHom 𝑦)) = ( I ↾ (𝑥 RngHom 𝑦)))
31	19, 30	eqtr2id 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ( I ↾ (𝑥 RngHom 𝑦)) = (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦))))
32	31	mpoeq3dva 7466	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦)))))
33	18, 32	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦)))))
34	7	a1i 11	. . . . . . 7 ⊢ (𝜑 → 𝐵 = (Base‘𝑅))
35	7	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐵 = (Base‘𝑅))
36		fvresi 7147	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑥) = 𝑥)
37	36	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (( I ↾ 𝐵)‘𝑥) = 𝑥)
38	37	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (( I ↾ 𝐵)‘𝑥) = 𝑥)
39		fvresi 7147	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐵 → (( I ↾ 𝐵)‘𝑦) = 𝑦)
40	39	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (( I ↾ 𝐵)‘𝑦) = 𝑦)
41	40	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (( I ↾ 𝐵)‘𝑦) = 𝑦)
42	38, 41	oveq12d 7405	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) = (𝑥(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))𝑦))
43		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))) = (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))))
44		simprr 772	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → 𝑧 = 𝑦)
45	44	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → (Base‘𝑧) = (Base‘𝑦))
46		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → 𝑤 = 𝑥)
47	46	fveq2d 6862	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → (Base‘𝑤) = (Base‘𝑥))
48	45, 47	oveq12d 7405	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → ((Base‘𝑧) ↑m (Base‘𝑤)) = ((Base‘𝑦) ↑m (Base‘𝑥)))
49	48	reseq2d 5950	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑤 = 𝑥 ∧ 𝑧 = 𝑦)) → ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))) = ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))
50	13	com12 32	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝐵 → (𝜑 → 𝑥 ∈ 𝑈))
51	50	adantr 480	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝜑 → 𝑥 ∈ 𝑈))
52	51	impcom 407	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝑈)
53	9	eleq2d 2814	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑦 ∈ 𝐵 ↔ 𝑦 ∈ (𝑈 ∩ Rng)))
54		elin 3930	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑈 ∩ Rng) ↔ (𝑦 ∈ 𝑈 ∧ 𝑦 ∈ Rng))
55	54	simplbi 497	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ (𝑈 ∩ Rng) → 𝑦 ∈ 𝑈)
56	53, 55	biimtrdi 253	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈))
57	56	a1d 25	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈)))
58	57	imp32 418	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝑈)
59		ovex 7420	. . . . . . . . . . . 12 ⊢ ((Base‘𝑦) ↑m (Base‘𝑥)) ∈ V
60	59	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((Base‘𝑦) ↑m (Base‘𝑥)) ∈ V)
61	60	resiexd 7190	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∈ V)
62	43, 49, 52, 58, 61	ovmpod 7541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))𝑦) = ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))))
63	42, 62	eqtr2d 2765	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) = ((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)))
64		eqidd 2730	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))))
65		oveq12 7396	. . . . . . . . . . . 12 ⊢ ((𝑓 = 𝑥 ∧ 𝑔 = 𝑦) → (𝑓 RngHom 𝑔) = (𝑥 RngHom 𝑦))
66	65	reseq2d 5950	. . . . . . . . . . 11 ⊢ ((𝑓 = 𝑥 ∧ 𝑔 = 𝑦) → ( I ↾ (𝑓 RngHom 𝑔)) = ( I ↾ (𝑥 RngHom 𝑦)))
67	66	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ (𝑓 = 𝑥 ∧ 𝑔 = 𝑦)) → ( I ↾ (𝑓 RngHom 𝑔)) = ( I ↾ (𝑥 RngHom 𝑦)))
68		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵)
69		simprr 772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵)
70		ovex 7420	. . . . . . . . . . . 12 ⊢ (𝑥 RngHom 𝑦) ∈ V
71	70	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 RngHom 𝑦) ∈ V)
72	71	resiexd 7190	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( I ↾ (𝑥 RngHom 𝑦)) ∈ V)
73	64, 67, 68, 69, 72	ovmpod 7541	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦) = ( I ↾ (𝑥 RngHom 𝑦)))
74	73	eqcomd 2735	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ( I ↾ (𝑥 RngHom 𝑦)) = (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦))
75	63, 74	coeq12d 5828	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦))) = (((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦)))
76	34, 35, 75	mpoeq123dva 7463	. . . . . 6 ⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑m (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHom 𝑦)))) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦))))
77	33, 76	eqtrd 2764	. . . . 5 ⊢ (𝜑 → 𝐺 = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦))))
78	17, 77	opeq12d 4845	. . . 4 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ = ⟨((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦)))⟩)
79		eqid 2729	. . . . 5 ⊢ (Base‘𝑅) = (Base‘𝑅)
80		eqid 2729	. . . . . 6 ⊢ (ExtStrCat‘𝑈) = (ExtStrCat‘𝑈)
81		eqidd 2730	. . . . . 6 ⊢ (𝜑 → ( I ↾ 𝐵) = ( I ↾ 𝐵))
82		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))))
83	6, 80, 7, 8, 81, 82	rngcifuestrc 20548	. . . . 5 ⊢ (𝜑 → ( I ↾ 𝐵)(𝑅 Func (ExtStrCat‘𝑈))(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))))
84		funcrngcsetcALT.s	. . . . . 6 ⊢ 𝑆 = (SetCat‘𝑈)
85		eqid 2729	. . . . . 6 ⊢ (Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈))
86		eqid 2729	. . . . . 6 ⊢ (Base‘𝑆) = (Base‘𝑆)
87	80, 8	estrcbas 18086	. . . . . . 7 ⊢ (𝜑 → 𝑈 = (Base‘(ExtStrCat‘𝑈)))
88	87	mpteq1d 5197	. . . . . 6 ⊢ (𝜑 → (𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑢)))
89		fveq2 6858	. . . . . . . . . . 11 ⊢ (𝑤 = 𝑢 → (Base‘𝑤) = (Base‘𝑢))
90	89	oveq2d 7403	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → ((Base‘𝑧) ↑m (Base‘𝑤)) = ((Base‘𝑧) ↑m (Base‘𝑢)))
91	90	reseq2d 5950	. . . . . . . . 9 ⊢ (𝑤 = 𝑢 → ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))) = ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑢))))
92		fveq2 6858	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑣 → (Base‘𝑧) = (Base‘𝑣))
93	92	oveq1d 7402	. . . . . . . . . 10 ⊢ (𝑧 = 𝑣 → ((Base‘𝑧) ↑m (Base‘𝑢)) = ((Base‘𝑣) ↑m (Base‘𝑢)))
94	93	reseq2d 5950	. . . . . . . . 9 ⊢ (𝑧 = 𝑣 → ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑢))) = ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢))))
95	91, 94	cbvmpov 7484	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))) = (𝑢 ∈ 𝑈, 𝑣 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢))))
96	95	a1i 11	. . . . . . 7 ⊢ (𝜑 → (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))) = (𝑢 ∈ 𝑈, 𝑣 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢)))))
97		eqidd 2730	. . . . . . . 8 ⊢ (𝜑 → ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢))) = ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢))))
98	87, 87, 97	mpoeq123dv 7464	. . . . . . 7 ⊢ (𝜑 → (𝑢 ∈ 𝑈, 𝑣 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢)))) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑣 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢)))))
99	96, 98	eqtrd 2764	. . . . . 6 ⊢ (𝜑 → (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑣 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑣) ↑m (Base‘𝑢)))))
100	80, 84, 85, 86, 8, 88, 99	funcestrcsetc 18110	. . . . 5 ⊢ (𝜑 → (𝑢 ∈ 𝑈 ↦ (Base‘𝑢))((ExtStrCat‘𝑈) Func 𝑆)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))))
101	79, 83, 100	cofuval2 17849	. . . 4 ⊢ (𝜑 → (⟨(𝑢 ∈ 𝑈 ↦ (Base‘𝑢)), (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))⟩) = ⟨((𝑢 ∈ 𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))𝑦)))⟩)
102	78, 101	eqtr4d 2767	. . 3 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ = (⟨(𝑢 ∈ 𝑈 ↦ (Base‘𝑢)), (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))⟩))
103		df-br 5108	. . . . 5 ⊢ (( I ↾ 𝐵)(𝑅 Func (ExtStrCat‘𝑈))(𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔))) ↔ ⟨( I ↾ 𝐵), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))⟩ ∈ (𝑅 Func (ExtStrCat‘𝑈)))
104	83, 103	sylib 218	. . . 4 ⊢ (𝜑 → ⟨( I ↾ 𝐵), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))⟩ ∈ (𝑅 Func (ExtStrCat‘𝑈)))
105		df-br 5108	. . . . 5 ⊢ ((𝑢 ∈ 𝑈 ↦ (Base‘𝑢))((ExtStrCat‘𝑈) Func 𝑆)(𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤)))) ↔ ⟨(𝑢 ∈ 𝑈 ↦ (Base‘𝑢)), (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
106	100, 105	sylib 218	. . . 4 ⊢ (𝜑 → ⟨(𝑢 ∈ 𝑈 ↦ (Base‘𝑢)), (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
107	104, 106	cofucl 17850	. . 3 ⊢ (𝜑 → (⟨(𝑢 ∈ 𝑈 ↦ (Base‘𝑢)), (𝑤 ∈ 𝑈, 𝑧 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑m (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ ( I ↾ (𝑓 RngHom 𝑔)))⟩) ∈ (𝑅 Func 𝑆))
108	102, 107	eqeltrd 2828	. 2 ⊢ (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
109		df-br 5108	. 2 ⊢ (𝐹(𝑅 Func 𝑆)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
110	108, 109	sylibr 234	1 ⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ∩ cin 3913  ⟨cop 4595   class class class wbr 5107   ↦ cmpt 5188   I cid 5532   ↾ cres 5640   ∘ ccom 5642  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387   ∈ cmpo 7389   ↑_m cmap 8799  WUnicwun 10653  Basecbs 17179   Func cfunc 17816   ∘_func ccofu 17818  SetCatcsetc 18037  ExtStrCatcestrc 18083  Rngcrng 20061   RngHom crnghm 20343  RngCatcrngc 20525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-er 8671  df-map 8801  df-pm 8802  df-ixp 8871  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-wun 10655  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-nn 12187  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254  df-8 12255  df-9 12256  df-n0 12443  df-z 12530  df-dec 12650  df-uz 12794  df-fz 13469  df-struct 17117  df-sets 17134  df-slot 17152  df-ndx 17164  df-base 17180  df-ress 17201  df-plusg 17233  df-hom 17244  df-cco 17245  df-0g 17404  df-cat 17629  df-cid 17630  df-homf 17631  df-ssc 17772  df-resc 17773  df-subc 17774  df-func 17820  df-idfu 17821  df-cofu 17822  df-full 17868  df-fth 17869  df-setc 18038  df-estrc 18084  df-mgm 18567  df-mgmhm 18619  df-sgrp 18646  df-mnd 18662  df-mhm 18710  df-grp 18868  df-ghm 19145  df-abl 19713  df-mgp 20050  df-rng 20062  df-rnghm 20345  df-rngc 20526

This theorem is referenced by: (None)