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 50481

Description: Lemma for sectpropd 50482. (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 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 17972	. . . . . . . 8 ⊢ Sect = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ {⟨𝑓, 𝑔⟩ ∣ [(Hom ‘𝑐) / ℎ]((𝑓 ∈ (𝑥ℎ𝑦) ∧ 𝑔 ∈ (𝑦ℎ𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑥)𝑓) = ((Id‘𝑐)‘𝑥))}))
8	7	mptrcl 7034	. . . . . . 7 ⊢ (𝑃 ∈ (Sect‘𝐶) → 𝐶 ∈ Cat)
9	8	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐶 ∈ Cat)
10	2, 3, 4, 5, 6, 9	sectffval 17975	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐶) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))}))
11		df-mpo 7456	. . . . 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 2866	. . 3 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑧 = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑥)) ∧ (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = ((Id‘𝐶)‘𝑥))})})
14		eloprab1st2nd 50310	. . 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 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 2852	. . . . . . . . . . . . . . . 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 7458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑥(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦))
26	25	eleq2d 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦)))
27		oveq2 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
28	27	eleq2d 2850	. . . . . . . . . . . . . . . . . . 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 4845	. . . . . . . . . . . . . . . . . . . . 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 7469	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥) = (⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃))))
33	32	oveqd 7468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (1^st ‘(1^st ‘𝑃)) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩(comp‘𝐶)(1^st ‘(1^st ‘𝑃)))𝑓))
34		fveq2 6916	. . . . . . . . . . . . . . . . . . 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 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 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 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 2852	. . . . . . . . . . . . . . . 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 7459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))))
43	42	eleq2d 2850	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)𝑦) ↔ 𝑓 ∈ ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃)))))
44		oveq1 7458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → (𝑦(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))))
45	44	eleq2d 2850	. . . . . . . . . . . . . . . . . . 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 4846	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = (2^nd ‘(1^st ‘𝑃)) → ⟨(1^st ‘(1^st ‘𝑃)), 𝑦⟩ = ⟨(1^st ‘(1^st ‘𝑃)), (2^nd ‘(1^st ‘𝑃))⟩)
48	47	oveq1d 7466	. . . . . . . . . . . . . . . . . . . 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 7468	. . . . . . . . . . . . . . . . . . 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 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 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 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 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 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 8109	. . . . . . . . . . . . 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 17932	. . . . . . . . 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 17920	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
67	59, 66	eleqtrd 2866	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (1^st ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
68	67	elfvexd 6952	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ V)
69	18, 21, 9, 68	cidpropd 17934	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Id‘𝐶) = (Id‘𝐷))
70	69	fveq1d 6918	. . . . . . . . . 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 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 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 2763	. . . . . . . . . . 11 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
75	2, 3, 74, 18, 59, 61	homfeqval 17921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐶)(2^nd ‘(1^st ‘𝑃))) = ((1^st ‘(1^st ‘𝑃))(Hom ‘𝐷)(2^nd ‘(1^st ‘𝑃))))
76	75	eleq2d 2850	. . . . . . . . 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 17921	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐶)(1^st ‘(1^st ‘𝑃))) = ((2^nd ‘(1^st ‘𝑃))(Hom ‘𝐷)(1^st ‘(1^st ‘𝑃))))
78	77	eleq2d 2850	. . . . . . . . 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 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 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 2763	. . . . . 6 ⊢ (Base‘𝐷) = (Base‘𝐷)
85		eqid 2763	. . . . . 6 ⊢ (Id‘𝐷) = (Id‘𝐷)
86		eqid 2763	. . . . . 6 ⊢ (Sect‘𝐷) = (Sect‘𝐷)
87	18, 21, 9, 68	catpropd 17933	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
88	9, 87	mpbid 235	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝐷 ∈ Cat)
89	61, 66	eleqtrd 2866	. . . . . 6 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (2^nd ‘(1^st ‘𝑃)) ∈ (Base‘𝐷))
90	84, 74, 16, 85, 86, 88, 67, 89	sectfval 17976	. . . . 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 50474	. . . . . 6 ⊢ (𝐷 ∈ Cat → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
93	88, 92	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → (Sect‘𝐷) Fn ((Base‘𝐷) × (Base‘𝐷)))
94		fnbrovb 7502	. . . . 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 5109	. . 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 2864	1 ⊢ ((𝜑 ∧ 𝑃 ∈ (Sect‘𝐶)) → 𝑃 ∈ (Sect‘𝐷))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2147 Vcvv 3454 [wsbc 3742 ⟨cop 4840 class class class wbr 5108 {copab 5173 × cxp 5656 Fn wfn 6561 ‘cfv 6566 (class class class)co 7451 {coprab 7452 ∈ cmpo 7453 1^st c1st 8033 2^nd c2nd 8034 Basecbs 17431 Hom chom 17483 compcco 17484 Catccat 17888 Idccid 17889 Hom_f chomf 17890 comp_fccomf 17891 Sectcsect 17969

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-id 5553 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-1st 8035 df-2nd 8036 df-cat 17892 df-cid 17893 df-homf 17894 df-comf 17895 df-sect 17972

This theorem is used by: sectpropd 50482

W3C validator