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 48998

Description: Lemma for sectpropd 48999. (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 484	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐶))
2		eqid 2729	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2729	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		eqid 2729	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
5		eqid 2729	. . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶)
6		eqid 2729	. . . . . 6 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
7		df-sect 17685	. . . . . . . 8 ⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
8	7	mptrcl 6959	. . . . . . 7 ⊢ (𝑃 ∈ (Sect‘𝐶) → 𝐶 ∈ Cat)
9	8	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐶 ∈ Cat)
10	2, 3, 4, 5, 6, 9	sectffval 17688	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}))
11		df-mpo 7374	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})}
12	10, 11	eqtrdi 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
13	1, 12	eleqtrd 2830	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
14		eloprab1st2nd 48829	. . 3 ⊢ (𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})} → 𝑃 = ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩)
15	13, 14	syl 17	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 = ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩)
16		eqid 2729	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
17		sectpropd.1	. . . . . . . . . . . 12 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
18	17	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
19	18	adantr 480	. . . . . . . . . 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 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (comp_f‘𝐶) = (comp_f‘𝐷))
22	21	adantr 480	. . . . . . . . . 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 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥 ∈ (Base‘𝐶) ↔ (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
24	23	anbi1d 631	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))))
25		oveq1 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦))
26	25	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦)))
27		oveq2 7377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
28	27	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↔ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
29	26, 28	anbi12d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ↔ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))))
30		opeq1 4833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ⟨𝑥, 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩)
31		id 22	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → 𝑥 = (1^st ‘(1^st ‘𝑃)))
32	30, 31	oveq12d 7387	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥) = (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
33	32	oveqd 7386	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓))
34		fveq2 6840	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((Id‘𝐶)‘𝑥) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))
35	33, 34	eqeq12d 2745	. . . . . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . . . . 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 5168	. . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . 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 2816	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦 ∈ (Base‘𝐶) ↔ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
41	40	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))))
42		oveq2 7377	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
43	42	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃)))))
44		oveq1 7376	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
45	44	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
46	43, 45	anbi12d 632	. . . . . . . . . . . . . . . . . 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 4834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩)
48	47	oveq1d 7384	. . . . . . . . . . . . . . . . . . . 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 7386	. . . . . . . . . . . . . . . . . . 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 2731	. . . . . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . . . . 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 5168	. . . . . . . . . . . . . . . 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 2740	. . . . . . . . . . . . . . 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 632	. . . . . . . . . . . . . 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 2733	. . . . . . . . . . . . . . 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 630	. . . . . . . . . . . . . 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 8021	. . . . . . . . . . . . 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 17	. . . . . . . . . . . 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 767	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
60	59	adantr 480	. . . . . . . . . 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 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
62	61	adantr 480	. . . . . . . . . 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 770	. . . . . . . . . 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 772	. . . . . . . . . 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 17645	. . . . . . . . 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 17633	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
67	59, 66	eleqtrd 2830	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
68	67	elfvexd 6879	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ V)
69	18, 21, 9, 68	cidpropd 17647	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Id‘𝐶) = (Id‘𝐷))
70	69	fveq1d 6842	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))
71	70	adantr 480	. . . . . . . . 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 2745	. . . . . . . 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 579	. . . . . . 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 2729	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
75	2, 3, 74, 18, 59, 61	homfeqval 17634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))))
76	75	eleq2d 2814	. . . . . . . . 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 17634	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))
78	77	eleq2d 2814	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))))
79	76, 78	anbi12d 632	. . . . . . . 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 631	. . . . . . 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 279	. . . . . 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 5168	. . . . 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 495	. . . . 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 2729	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
85		eqid 2729	. . . . . 6 ⊢ (Id‘𝐷) = (Id‘𝐷)
86		eqid 2729	. . . . . 6 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
87	18, 21, 9, 68	catpropd 17646	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
88	9, 87	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ Cat)
89	61, 66	eleqtrd 2830	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
90	84, 74, 16, 85, 86, 88, 67, 89	sectfval 17689	. . . . 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 2775	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃))
92		sectfn 48991	. . . . . 6 ⊢ (𝐷 ∈ Cat → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
93	88, 92	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
94		fnbrovb 7420	. . . . 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 836	. . . 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 232	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩(Sect‘𝐷)(2^nd ‘𝑃))
97		df-br 5103	. . 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 218	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩ ∈ (Sect‘𝐷))
99	15, 98	eqeltrd 2828	1 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 Vcvv 3444 [wsbc 3750 ⟨cop 4591 class class class wbr 5102 {copab 5164 × cxp 5629 Fn wfn 6494 ‘cfv 6499 (class class class)co 7369 {coprab 7370 ∈ cmpo 7371 1^st c1st 7945 2^nd c2nd 7946 Basecbs 17155 Hom chom 17207 compcco 17208 Catccat 17601 Idccid 17602 Hom_f chomf 17603 comp_fccomf 17604 Sectcsect 17682

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 5229 ax-sep 5246 ax-nul 5256 ax-pow 5315 ax-pr 5382 ax-un 7691

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 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-ral 3045 df-rex 3054 df-reu 3352 df-rab 3403 df-v 3446 df-sbc 3751 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4293 df-if 4485 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5526 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6452 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-riota 7326 df-ov 7372 df-oprab 7373 df-mpo 7374 df-1st 7947 df-2nd 7948 df-cat 17605 df-cid 17606 df-homf 17607 df-comf 17608 df-sect 17685

This theorem is referenced by: sectpropd 48999

W3C validator