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 50244

Description: Lemma for sectpropd 50245. (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 490	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐶))
2		eqid 2760	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2760	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		eqid 2760	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
5		eqid 2760	. . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶)
6		eqid 2760	. . . . . 6 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
7		df-sect 17928	. . . . . . . 8 ⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
8	7	mptrcl 7004	. . . . . . 7 ⊢ (𝑃 ∈ (Sect‘𝐶) → 𝐶 ∈ Cat)
9	8	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐶 ∈ Cat)
10	2, 3, 4, 5, 6, 9	sectffval 17931	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}))
11		df-mpo 7426	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})}
12	10, 11	eqtrdi 2811	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
13	1, 12	eleqtrd 2862	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
14		eloprab1st2nd 50073	. . 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 2760	. . . . . . . . . 10 ⊢ (comp‘𝐷) = (comp‘𝐷)
17		sectpropd.1	. . . . . . . . . . . 12 ⊢ (𝜑 → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
18	17	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Hom_f ‘𝐶) = (Hom_f ‘𝐷))
19	18	adantr 486	. . . . . . . . . 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 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (comp_f‘𝐶) = (comp_f‘𝐷))
22	21	adantr 486	. . . . . . . . . 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 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥 ∈ (Base‘𝐶) ↔ (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
24	23	anbi1d 643	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))))
25		oveq1 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦))
26	25	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦)))
27		oveq2 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
28	27	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥) ↔ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
29	26, 28	anbi12d 644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ↔ (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))))
30		opeq1 4839	. . . . . . . . . . . . . . . . . . . . 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 7439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥) = (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
33	32	oveqd 7438	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓))
34		fveq2 6886	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → ((Id‘𝐶)‘𝑥) = ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))))
35	33, 34	eqeq12d 2776	. . . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . . 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 5170	. . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . 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 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦 ∈ (Base‘𝐶) ↔ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶)))
41	40	anbi2d 642	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ↔ ((1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶) ∧ (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))))
42		oveq2 7429	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
43	42	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃)))))
44		oveq1 7428	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
45	44	eleq2d 2846	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑔 ∈ (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃)))))
46	43, 45	anbi12d 644	. . . . . . . . . . . . . . . . . 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 4840	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩)
48	47	oveq1d 7436	. . . . . . . . . . . . . . . . . . . 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 7438	. . . . . . . . . . . . . . . . . . 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 2762	. . . . . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . . . . 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 5170	. . . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . . . 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 644	. . . . . . . . . . . . . 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 2764	. . . . . . . . . . . . . . 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 642	. . . . . . . . . . . . . 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 8075	. . . . . . . . . . . . 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 780	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
60	59	adantr 486	. . . . . . . . . 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 782	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐶))
62	61	adantr 486	. . . . . . . . . 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 783	. . . . . . . . . 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 785	. . . . . . . . . 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 17888	. . . . . . . . 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 17876	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
67	59, 66	eleqtrd 2862	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
68	67	elfvexd 6922	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ V)
69	18, 21, 9, 68	cidpropd 17890	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Id‘𝐶) = (Id‘𝐷))
70	69	fveq1d 6888	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((Id‘𝐶)‘(1^st ‘(1^st ‘𝑃))) = ((Id‘𝐷)‘(1^st ‘(1^st ‘𝑃))))
71	70	adantr 486	. . . . . . . . 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 2776	. . . . . . . 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 590	. . . . . . 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 2760	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
75	2, 3, 74, 18, 59, 61	homfeqval 17877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))))
76	75	eleq2d 2846	. . . . . . . . 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 17877	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))
78	77	eleq2d 2846	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) ↔ 𝑔 ∈ ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃)))))
79	76, 78	anbi12d 644	. . . . . . . 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 643	. . . . . . 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 5170	. . . . 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 501	. . . . 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 2760	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
85		eqid 2760	. . . . . 6 ⊢ (Id‘𝐷) = (Id‘𝐷)
86		eqid 2760	. . . . . 6 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
87	18, 21, 9, 68	catpropd 17889	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
88	9, 87	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ Cat)
89	61, 66	eleqtrd 2862	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
90	84, 74, 16, 85, 86, 88, 67, 89	sectfval 17932	. . . . 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 2806	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃))
92		sectfn 50237	. . . . . 6 ⊢ (𝐷 ∈ Cat → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
93	88, 92	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
94		fnbrovb 7472	. . . . 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 850	. . . 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 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 221	. 2 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ⟨⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩, (2^nd ‘𝑃)⟩ ∈ (Sect‘𝐷))
99	15, 98	eqeltrd 2860	1 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1569 ∈ wcel 2144 Vcvv 3450 [wsbc 3738 ⟨cop 4834 class class class wbr 5102 {copab 5166 × cxp 5648 Fn wfn 6534 ‘cfv 6539 (class class class)co 7421 {coprab 7422 ∈ cmpo 7423 1^st c1st 8000 2^nd c2nd 8001 Basecbs 17393 Hom chom 17445 compcco 17446 Catccat 17844 Idccid 17845 Hom_f chomf 17846 comp_fccomf 17847 Sectcsect 17925

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-1st 8002 df-2nd 8003 df-cat 17848 df-cid 17849 df-homf 17850 df-comf 17851 df-sect 17928

This theorem is used by: sectpropd 50245

W3C validator