sectpropdlem - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sectpropdlem		Structured version Visualization version GIF version

Theorem sectpropdlem 49814

Description: Lemma for sectpropd 49815. (Contributed by Zhi Wang, 27-Oct-2025.)

**Hypotheses**
Ref	Expression
sectpropd.1	⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
sectpropd.2	⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))

**Assertion**
Ref	Expression
sectpropdlem	⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Proof of Theorem sectpropdlem Dummy variables 𝑐 𝑓 𝑔 ℎ 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐶))
2		eqid 2763	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2763	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		eqid 2763	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
5		eqid 2763	. . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶)
6		eqid 2763	. . . . . 6 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
7		df-sect 17799	. . . . . . . 8 ⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
8	7	mptrcl 6999	. . . . . . 7 ⊢ (𝑃 ∈ (Sect‘𝐶) → 𝐶 ∈ Cat)
9	8	adantl 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐶 ∈ Cat)
10	2, 3, 4, 5, 6, 9	sectffval 17802	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}))
11		df-mpo 7415	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})}
12	10, 11	eqtrdi 2814	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
13	1, 12	eleqtrd 2865	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
14		eloprab1st2nd 49646	. . 3 ⊢ (𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})} → 𝑃 = ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩)
15	13, 14	syl 18	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 = ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩)
16		eqid 2763	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
17		sectpropd.1	. . . . . . . . . . . 12 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
18	17	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
19	18	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
20		sectpropd.2	. . . . . . . . . . . 12 ⊢ (𝜑 → (comp_f‘𝐶) = (comp_f‘𝐷))
21	20	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (comp_f‘𝐶) = (comp_f‘𝐷))
22	21	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → (comp_f‘𝐶) = (comp_f‘𝐷))
23		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥 ∈ (Base‘𝐶) ↔ (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
24	23	anbi1d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))))
25		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦))
26	25	eleq2d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦)))
27		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
28	27	eleq2d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↔ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
29	26, 28	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ↔ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))))
30		opeq1 4838	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ⟨𝑥, 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩)
31		id 23	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → 𝑥 = (1^st ‘(1^st ‘𝑃)))
32	30, 31	oveq12d 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥) = (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
33	32	oveqd 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓))
34		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((Id‘𝐶)‘𝑥) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))
35	33, 34	eqeq12d 2779	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥) ↔ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃)))))
36	29, 35	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥)) ↔ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))))
37	36	opabbidv 5177	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})
38	37	eqeq2d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))} ↔ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}))
39	24, 38	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}) ↔ (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})))
40		eleq1 2851	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦 ∈ (Base‘𝐶) ↔ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
41	40	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))))
42		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
43	42	eleq2d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃)))))
44		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
45	44	eleq2d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
46	43, 45	anbi12d 643	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ↔ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))))
47		opeq2 4839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩)
48	47	oveq1d 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))) = (⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
49	48	oveqd 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓))
50	49	eqeq1d 2765	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) ↔ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃)))))
51	46, 50	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃)))) ↔ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))))
52	51	opabbidv 5177	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})
53	52	eqeq2d 2774	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))} ↔ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}))
54	41, 53	anbi12d 643	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}) ↔ (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})))
55		eqeq1 2767	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = (2^nd ‘𝑃) → (𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))} ↔ (2^nd ‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}))
56	55	anbi2d 641	. . . . . . . . . . . . . 14 ⊢ (𝑧 = (2^nd ‘𝑃) → ((((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}) ↔ (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)) ∧ (2^nd ‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})))
57	39, 54, 56	eloprabi 8056	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})} → (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)) ∧ (2^nd ‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}))
58	13, 57	syl 18	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)) ∧ (2^nd ‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))}))
59	58	simplld 779	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
60	59	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
61	58	simplrd 781	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
62	61	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
63		simprl 782	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
64		simprr 784	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
65	2, 3, 4, 16, 19, 22, 60, 62, 60, 63, 64	comfeqval 17759	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓))
66	18	homfeqbas 17747	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
67	59, 66	eleqtrd 2865	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
68	67	elfvexd 6917	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ V)
69	18, 21, 9, 68	cidpropd 17761	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Id‘𝐶) = (Id‘𝐷))
70	69	fveq1d 6883	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))
71	70	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))
72	65, 71	eqeq12d 2779	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) ∧ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))) → ((𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) ↔ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃)))))
73	72	pm5.32da 589	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃)))) ↔ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))))
74		eqid 2763	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
75	2, 3, 74, 18, 59, 61	homfeqval 17748	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))))
76	75	eleq2d 2849	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃)))))
77	2, 3, 74, 18, 61, 59	homfeqval 17748	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))
78	77	eleq2d 2849	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))))
79	76, 78	anbi12d 643	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ↔ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))))
80	79	anbi1d 642	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃)))) ↔ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))))
81	73, 80	bitrd 282	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃)))) ↔ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))))
82	81	opabbidv 5177	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))} = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))})
83	58	simprd 500	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘𝑃) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))})
84		eqid 2763	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
85		eqid 2763	. . . . . 6 ⊢ (Id‘𝐷) = (Id‘𝐷)
86		eqid 2763	. . . . . 6 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
87	18, 21, 9, 68	catpropd 17760	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
88	9, 87	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ Cat)
89	61, 66	eleqtrd 2865	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
90	84, 74, 16, 85, 86, 88, 67, 89	sectfval 17803	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))) ∧ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))) ∧ (𝑔(⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(comp‘𝐷)(1^st ‘(1^st ‘𝑃)))𝑓) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))})
91	82, 83, 90	3eqtr4rd 2809	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃))
92		sectfn 49807	. . . . . 6 ⊢ (𝐷 ∈ Cat → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
93	88, 92	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
94		fnbrovb 7461	. . . . 5 ⊢ (((Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)) ∧ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))) → (((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃) ↔ ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(Sect‘𝐷)(2^nd ‘𝑃)))
95	93, 67, 89, 94	syl12anc 849	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃) ↔ ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(Sect‘𝐷)(2^nd ‘𝑃)))
96	91, 95	mpbid 235	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(Sect‘𝐷)(2^nd ‘𝑃))
97		df-br 5110	. . 3 ⊢ (⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(Sect‘𝐷)(2^nd ‘𝑃) ↔ ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩ ∈ (Sect‘𝐷))
98	96, 97	sylib 221	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩ ∈ (Sect‘𝐷))
99	15, 98	eqeltrd 2863	1 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 Vcvv 3455 [wsbc 3744 ⟨cop 4595 class class class wbr 5109 {copab 5173 × cxp 5659 Fn wfn 6531 ‘cfv 6536 (class class class)co 7410 {coprab 7411 ∈ cmpo 7412 1^st c1st 7980 2^nd c2nd 7981 Basecbs 17264 Hom chom 17316 compcco 17317 Catccat 17715 Idccid 17716 Hom_f chomf 17717 comp_fccomf 17718 Sectcsect 17796

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7982 df-2nd 7983 df-cat 17719 df-cid 17720 df-homf 17721 df-comf 17722 df-sect 17799

This theorem is referenced by: sectpropd 49815

W3C validator