sectpropdlem

	Ref	Expression
Hypotheses	sectpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	sectpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
Assertion	sectpropdlem	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝑃 ∈ ( Sect ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
2		sectpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
3		simpr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝑃 ∈ ( Sect ‘ 𝐶 ) )
4		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
6		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
7		eqid	⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
8		eqid	⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
9		df-sect	⊢ Sect = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) , 𝑦 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Hom ‘ 𝑐 ) / ℎ ] ( ( 𝑓 ∈ ( 𝑥 ℎ 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ℎ 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ) } ) )
10	9	mptrcl	⊢ ( 𝑃 ∈ ( Sect ‘ 𝐶 ) → 𝐶 ∈ Cat )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
12	4 5 6 7 8 11	sectffval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Sect ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) )
13		df-mpo	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) }
14	12 13	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Sect ‘ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) } )
15	3 14	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) } )
16		eloprab1st2nd	⊢ ( 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑧 = { ⟨ 𝑓 , 𝑔 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ∧ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ) } ) } → 𝑃 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ )
17	15 16	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝑃 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ )
18		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
20	19	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) ∧ ( 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
21	2	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↔ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) )
24	23	anbi1d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) )
25		oveq1	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) 𝑦 ) )
26	25	eleq2d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) 𝑦 ) ) )
27		oveq2	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
28	27	eleq2d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
29	26 28	anbi12d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ) ↔ ( 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) ) )
30		opeq1	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , 𝑦 ⟩ )
31		id	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) )
32	30 31	oveq12d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) = ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , 𝑦 ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
33	32	oveqd	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( 𝑔 ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , 𝑦 ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) 𝑓 ) )
34		fveq2	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) = ( ( Id ‘ 𝐶 ) ‘ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
35	33 34	eqeq12d	⊢ ( 𝑥 = ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ↔ ( 𝑔 ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , 𝑦 ⟩ ( comp ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) 𝑓 ) = ( ( Id ‘ 𝐶 ) ‘ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
36	29 35	anbi12d	⊢ ( 𝑥 = ( 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	⊢ ( 𝑥 = ( 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	⊢ ( 𝑥 = ( 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	⊢ ( 𝑥 = ( 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	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ∈ ( Base ‘ 𝐶 ) ↔ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) )
41	40	anbi2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ↔ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ∧ ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) ) ) )
42		oveq2	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) 𝑦 ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) )
43	42	eleq2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) 𝑦 ) ↔ 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
44		oveq1	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑦 ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
45	44	eleq2d	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ( 𝑔 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ↔ 𝑔 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
46	43 45	anbi12d	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , 𝑦 ⟩ = ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ )
48	47	oveq1d	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑦 = ( 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	⊢ ( 𝑧 = ( 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	⊢ ( 𝑧 = ( 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	⊢ ( 𝑃 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ ( 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	15 57	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) )
60	59	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐶 ) )
62	61	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	4 5 6 18 20 22 60 62 60 63 64	comfeqval	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	19	homfeqbas	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
67	59 66	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) )
68	67	elfvexd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝐷 ∈ V )
69	19 21 11 68	cidpropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Id ‘ 𝐶 ) = ( Id ‘ 𝐷 ) )
70	69	fveq1d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( ( Id ‘ 𝐶 ) ‘ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
71	70	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
75	4 5 74 19 59 61	homfeqval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) )
76	75	eleq2d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ↔ 𝑓 ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
77	4 5 74 19 61 59	homfeqval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) = ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) )
78	77	eleq2d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 𝑔 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐶 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ↔ 𝑔 ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ( Hom ‘ 𝐷 ) ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ) ) )
79	76 78	anbi12d	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
85		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
86		eqid	⊢ ( Sect ‘ 𝐷 ) = ( Sect ‘ 𝐷 )
87	19 21 11 68	catpropd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
88	11 87	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
89	61 66	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ∈ ( Base ‘ 𝐷 ) )
90	84 74 18 85 86 88 67 89	sectfval	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) ( Sect ‘ 𝐷 ) ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ) = ( 2^nd ‘ 𝑃 ) )
92		sectfn	⊢ ( 𝐷 ∈ Cat → ( Sect ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
93	88 92	syl	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ( Sect ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
94		fnbrovb	⊢ ( ( ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ ( Sect ‘ 𝐷 ) ( 2^nd ‘ 𝑃 ) )
97		df-br	⊢ ( ⟨ ( 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	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑃 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑃 ) ) ⟩ , ( 2^nd ‘ 𝑃 ) ⟩ ∈ ( Sect ‘ 𝐷 ) )
99	17 98	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑃 ∈ ( Sect ‘ 𝐶 ) ) → 𝑃 ∈ ( Sect ‘ 𝐷 ) )

Metamath Proof Explorer

Theorem sectpropdlem

Proof