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 48910

Description: Lemma for sectpropd 48911. (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 2734	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
3		eqid 2734	. . . . . 6 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
4		eqid 2734	. . . . . 6 ⊢ (comp‘𝐶) = (comp‘𝐶)
5		eqid 2734	. . . . . 6 ⊢ (Id‘𝐶) = (Id‘𝐶)
6		eqid 2734	. . . . . 6 ⊢ (Sect‘𝐶) = (Sect‘𝐶)
7		df-sect 17763	. . . . . . . 8 ⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
8	7	mptrcl 7005	. . . . . . 7 ⊢ (𝑃 ∈ (Sect‘𝐶) → 𝐶 ∈ Cat)
9	8	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐶 ∈ Cat)
10	2, 3, 4, 5, 6, 9	sectffval 17766	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}))
11		df-mpo 7418	. . . . 5 ⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})}
12	10, 11	eqtrdi 2785	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
13	1, 12	eleqtrd 2835	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
14		eloprab1st2nd 48751	. . 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 2734	. . . . . . . . . 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 2821	. . . . . . . . . . . . . . . 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 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦))
26	25	eleq2d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦)))
27		oveq2 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
28	27	eleq2d 2819	. . . . . . . . . . . . . . . . . . 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 4853	. . . . . . . . . . . . . . . . . . . . 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 7431	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥) = (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
33	32	oveqd 7430	. . . . . . . . . . . . . . . . . . 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 2750	. . . . . . . . . . . . . . . . . 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 5189	. . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . 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 2821	. . . . . . . . . . . . . . . 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 7421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
43	42	eleq2d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃)))))
44		oveq1 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
45	44	eleq2d 2819	. . . . . . . . . . . . . . . . . . 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 4854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩)
48	47	oveq1d 7428	. . . . . . . . . . . . . . . . . . . 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 7430	. . . . . . . . . . . . . . . . . . 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 2736	. . . . . . . . . . . . . . . . . 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 5189	. . . . . . . . . . . . . . . 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 2745	. . . . . . . . . . . . . . 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 2738	. . . . . . . . . . . . . . 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 8070	. . . . . . . . . . . . 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 17723	. . . . . . . . 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 17711	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
67	59, 66	eleqtrd 2835	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
68	67	elfvexd 6925	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ V)
69	18, 21, 9, 68	cidpropd 17725	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Id‘𝐶) = (Id‘𝐷))
70	69	fveq1d 6888	. . . . . . . . . 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 2750	. . . . . . . 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 2734	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
75	2, 3, 74, 18, 59, 61	homfeqval 17712	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))))
76	75	eleq2d 2819	. . . . . . . . 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 17712	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))
78	77	eleq2d 2819	. . . . . . . . 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 5189	. . . . 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 2734	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
85		eqid 2734	. . . . . 6 ⊢ (Id‘𝐷) = (Id‘𝐷)
86		eqid 2734	. . . . . 6 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
87	18, 21, 9, 68	catpropd 17724	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
88	9, 87	mpbid 232	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ Cat)
89	61, 66	eleqtrd 2835	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
90	84, 74, 16, 85, 86, 88, 67, 89	sectfval 17767	. . . . 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 2780	. . . 4 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Sect‘𝐷)(2^nd ‘(1^st ‘𝑃))) = (2^nd ‘𝑃))
92		sectfn 48906	. . . . . 6 ⊢ (𝐷 ∈ Cat → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
93	88, 92	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
94		fnbrovb 7464	. . . . 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 5124	. . 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 2833	1 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 Vcvv 3463 [wsbc 3770 ⟨cop 4612 class class class wbr 5123 {copab 5185 × cxp 5663 Fn wfn 6536 ‘cfv 6541 (class class class)co 7413 {coprab 7414 ∈ cmpo 7415 1^st c1st 7994 2^nd c2nd 7995 Basecbs 17230 Hom chom 17285 compcco 17286 Catccat 17679 Idccid 17680 Hom_f chomf 17681 comp_fccomf 17682 Sectcsect 17760

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-ral 3051 df-rex 3060 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-id 5558 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-1st 7996 df-2nd 7997 df-cat 17683 df-cid 17684 df-homf 17685 df-comf 17686 df-sect 17763

This theorem is referenced by: sectpropd 48911

W3C validator