sectpropdlem

	Ref	Expression
Hypotheses	sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	sectpropdlem	$⊢ (φ \land P \in Sect (C)) \to P \in Sect (D)$

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		sectpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		simpr	$⊢ (φ \land P \in Sect (C)) \to P \in Sect (C)$
4		eqid	$⊢ {Base}_{C} = {Base}_{C}$
5		eqid	$⊢ Hom (C) = Hom (C)$
6		eqid	$⊢ comp (C) = comp (C)$
7		eqid	$⊢ Id (C) = Id (C)$
8		eqid	$⊢ Sect (C) = Sect (C)$
9		df-sect	$⊢ Sect = (c \in Cat ⟼ (x \in {Base}_{c}, y \in {Base}_{c} ⟼ \{⟨f, g⟩ \| \underset{˙}{[} Hom (c) / h \underset{˙}{]} ((f \in (x h y) \land g \in (y h x)) \land g (⟨x, y⟩ comp (c) x) f = Id (c) (x))\}))$
10	9	mptrcl	$⊢ P \in Sect (C) \to C \in Cat$
11	10	adantl	$⊢ (φ \land P \in Sect (C)) \to C \in Cat$
12	4 5 6 7 8 11	sectffval	$⊢ (φ \land P \in Sect (C)) \to Sect (C) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})$
13		df-mpo	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})\}$
14	12 13	eqtrdi	$⊢ (φ \land P \in Sect (C)) \to Sect (C) = \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})\}$
15	3 14	eleqtrd	$⊢ (φ \land P \in Sect (C)) \to P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})\}$
16		eloprab1st2nd	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})\} \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
17	15 16	syl	$⊢ (φ \land P \in Sect (C)) \to P = ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩$
18		eqid	$⊢ comp (D) = comp (D)$
19	1	adantr	$⊢ (φ \land P \in Sect (C)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
20	19	adantr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
21	2	adantr	$⊢ (φ \land P \in Sect (C)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
22	21	adantr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
23		eleq1	$⊢ x = 1^{st} (1^{st} (P)) \to (x \in {Base}_{C} \leftrightarrow 1^{st} (1^{st} (P)) \in {Base}_{C})$
24	23	anbi1d	$⊢ x = 1^{st} (1^{st} (P)) \to ((x \in {Base}_{C} \land y \in {Base}_{C}) \leftrightarrow (1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}))$
25		oveq1	$⊢ x = 1^{st} (1^{st} (P)) \to x Hom (C) y = 1^{st} (1^{st} (P)) Hom (C) y$
26	25	eleq2d	$⊢ x = 1^{st} (1^{st} (P)) \to (f \in (x Hom (C) y) \leftrightarrow f \in (1^{st} (1^{st} (P)) Hom (C) y))$
27		oveq2	$⊢ x = 1^{st} (1^{st} (P)) \to y Hom (C) x = y Hom (C) 1^{st} (1^{st} (P))$
28	27	eleq2d	$⊢ x = 1^{st} (1^{st} (P)) \to (g \in (y Hom (C) x) \leftrightarrow g \in (y Hom (C) 1^{st} (1^{st} (P))))$
29	26 28	anbi12d	$⊢ x = 1^{st} (1^{st} (P)) \to ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \leftrightarrow (f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))))$
30		opeq1	$⊢ x = 1^{st} (1^{st} (P)) \to ⟨x, y⟩ = ⟨1^{st} (1^{st} (P)), y⟩$
31		id	$⊢ x = 1^{st} (1^{st} (P)) \to x = 1^{st} (1^{st} (P))$
32	30 31	oveq12d	$⊢ x = 1^{st} (1^{st} (P)) \to ⟨x, y⟩ comp (C) x = ⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))$
33	32	oveqd	$⊢ x = 1^{st} (1^{st} (P)) \to g (⟨x, y⟩ comp (C) x) f = g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f$
34		fveq2	$⊢ x = 1^{st} (1^{st} (P)) \to Id (C) (x) = Id (C) (1^{st} (1^{st} (P)))$
35	33 34	eqeq12d	$⊢ x = 1^{st} (1^{st} (P)) \to (g (⟨x, y⟩ comp (C) x) f = Id (C) (x) \leftrightarrow g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))$
36	29 35	anbi12d	$⊢ x = 1^{st} (1^{st} (P)) \to (((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x)) \leftrightarrow ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P)))))$
37	36	opabbidv	$⊢ x = 1^{st} (1^{st} (P)) \to \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\} = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}$
38	37	eqeq2d	$⊢ x = 1^{st} (1^{st} (P)) \to (z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\} \leftrightarrow z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\})$
39	24 38	anbi12d	$⊢ x = 1^{st} (1^{st} (P)) \to (((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}))$
40		eleq1	$⊢ y = 2^{nd} (1^{st} (P)) \to (y \in {Base}_{C} \leftrightarrow 2^{nd} (1^{st} (P)) \in {Base}_{C})$
41	40	anbi2d	$⊢ y = 2^{nd} (1^{st} (P)) \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \leftrightarrow (1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}))$
42		oveq2	$⊢ y = 2^{nd} (1^{st} (P)) \to 1^{st} (1^{st} (P)) Hom (C) y = 1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))$
43	42	eleq2d	$⊢ y = 2^{nd} (1^{st} (P)) \to (f \in (1^{st} (1^{st} (P)) Hom (C) y) \leftrightarrow f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))))$
44		oveq1	$⊢ y = 2^{nd} (1^{st} (P)) \to y Hom (C) 1^{st} (1^{st} (P)) = 2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))$
45	44	eleq2d	$⊢ y = 2^{nd} (1^{st} (P)) \to (g \in (y Hom (C) 1^{st} (1^{st} (P))) \leftrightarrow g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))$
46	43 45	anbi12d	$⊢ y = 2^{nd} (1^{st} (P)) \to ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \leftrightarrow (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))))$
47		opeq2	$⊢ y = 2^{nd} (1^{st} (P)) \to ⟨1^{st} (1^{st} (P)), y⟩ = ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩$
48	47	oveq1d	$⊢ y = 2^{nd} (1^{st} (P)) \to ⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P)) = ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))$
49	48	oveqd	$⊢ y = 2^{nd} (1^{st} (P)) \to g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f$
50	49	eqeq1d	$⊢ y = 2^{nd} (1^{st} (P)) \to (g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))) \leftrightarrow g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))$
51	46 50	anbi12d	$⊢ y = 2^{nd} (1^{st} (P)) \to (((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P)))) \leftrightarrow ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P)))))$
52	51	opabbidv	$⊢ y = 2^{nd} (1^{st} (P)) \to \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\} = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}$
53	52	eqeq2d	$⊢ y = 2^{nd} (1^{st} (P)) \to (z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\} \leftrightarrow z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\})$
54	41 53	anbi12d	$⊢ y = 2^{nd} (1^{st} (P)) \to (((1^{st} (1^{st} (P)) \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) y) \land g \in (y Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), y⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}))$
55		eqeq1	$⊢ z = 2^{nd} (P) \to (z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\} \leftrightarrow 2^{nd} (P) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\})$
56	55	anbi2d	$⊢ z = 2^{nd} (P) \to (((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}) \leftrightarrow ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}))$
57	39 54 56	eloprabi	$⊢ P \in \{⟨⟨x, y⟩, z⟩ \| ((x \in {Base}_{C} \land y \in {Base}_{C}) \land z = \{⟨f, g⟩ \| ((f \in (x Hom (C) y) \land g \in (y Hom (C) x)) \land g (⟨x, y⟩ comp (C) x) f = Id (C) (x))\})\} \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\})$
58	15 57	syl	$⊢ (φ \land P \in Sect (C)) \to ((1^{st} (1^{st} (P)) \in {Base}_{C} \land 2^{nd} (1^{st} (P)) \in {Base}_{C}) \land 2^{nd} (P) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\})$
59	58	simplld	$⊢ (φ \land P \in Sect (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{C}$
60	59	adantr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to 1^{st} (1^{st} (P)) \in {Base}_{C}$
61	58	simplrd	$⊢ (φ \land P \in Sect (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{C}$
62	61	adantr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to 2^{nd} (1^{st} (P)) \in {Base}_{C}$
63		simprl	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P)))$
64		simprr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))$
65	4 5 6 18 20 22 60 62 60 63 64	comfeqval	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f$
66	19	homfeqbas	$⊢ (φ \land P \in Sect (C)) \to {Base}_{C} = {Base}_{D}$
67	59 66	eleqtrd	$⊢ (φ \land P \in Sect (C)) \to 1^{st} (1^{st} (P)) \in {Base}_{D}$
68	67	elfvexd	$⊢ (φ \land P \in Sect (C)) \to D \in V$
69	19 21 11 68	cidpropd	$⊢ (φ \land P \in Sect (C)) \to Id (C) = Id (D)$
70	69	fveq1d	$⊢ (φ \land P \in Sect (C)) \to Id (C) (1^{st} (1^{st} (P))) = Id (D) (1^{st} (1^{st} (P)))$
71	70	adantr	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to Id (C) (1^{st} (1^{st} (P))) = Id (D) (1^{st} (1^{st} (P)))$
72	65 71	eqeq12d	$⊢ ((φ \land P \in Sect (C)) \land (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))))) \to (g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))) \leftrightarrow g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P))))$
73	72	pm5.32da	$⊢ (φ \land P \in Sect (C)) \to (((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P)))) \leftrightarrow ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P)))))$
74		eqid	$⊢ Hom (D) = Hom (D)$
75	4 5 74 19 59 61	homfeqval	$⊢ (φ \land P \in Sect (C)) \to 1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P)) = 1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))$
76	75	eleq2d	$⊢ (φ \land P \in Sect (C)) \to (f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \leftrightarrow f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))))$
77	4 5 74 19 61 59	homfeqval	$⊢ (φ \land P \in Sect (C)) \to 2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)) = 2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P))$
78	77	eleq2d	$⊢ (φ \land P \in Sect (C)) \to (g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P))) \leftrightarrow g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P))))$
79	76 78	anbi12d	$⊢ (φ \land P \in Sect (C)) \to ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \leftrightarrow (f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P)))))$
80	79	anbi1d	$⊢ (φ \land P \in Sect (C)) \to (((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P)))) \leftrightarrow ((f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P)))))$
81	73 80	bitrd	$⊢ (φ \land P \in Sect (C)) \to (((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P)))) \leftrightarrow ((f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P)))))$
82	81	opabbidv	$⊢ (φ \land P \in Sect (C)) \to \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\} = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P))))\}$
83	58	simprd	$⊢ (φ \land P \in Sect (C)) \to 2^{nd} (P) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (C) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (C) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (C) 1^{st} (1^{st} (P))) f = Id (C) (1^{st} (1^{st} (P))))\}$
84		eqid	$⊢ {Base}_{D} = {Base}_{D}$
85		eqid	$⊢ Id (D) = Id (D)$
86		eqid	$⊢ Sect (D) = Sect (D)$
87	19 21 11 68	catpropd	$⊢ (φ \land P \in Sect (C)) \to (C \in Cat \leftrightarrow D \in Cat)$
88	11 87	mpbid	$⊢ (φ \land P \in Sect (C)) \to D \in Cat$
89	61 66	eleqtrd	$⊢ (φ \land P \in Sect (C)) \to 2^{nd} (1^{st} (P)) \in {Base}_{D}$
90	84 74 18 85 86 88 67 89	sectfval	$⊢ (φ \land P \in Sect (C)) \to 1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P)) = \{⟨f, g⟩ \| ((f \in (1^{st} (1^{st} (P)) Hom (D) 2^{nd} (1^{st} (P))) \land g \in (2^{nd} (1^{st} (P)) Hom (D) 1^{st} (1^{st} (P)))) \land g (⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ comp (D) 1^{st} (1^{st} (P))) f = Id (D) (1^{st} (1^{st} (P))))\}$
91	82 83 90	3eqtr4rd	$⊢ (φ \land P \in Sect (C)) \to 1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P)$
92		sectfn	$⊢ D \in Cat \to Sect (D) Fn ({Base}_{D} \times {Base}_{D})$
93	88 92	syl	$⊢ (φ \land P \in Sect (C)) \to Sect (D) Fn ({Base}_{D} \times {Base}_{D})$
94		fnbrovb	$⊢ (Sect (D) Fn ({Base}_{D} \times {Base}_{D}) \land (1^{st} (1^{st} (P)) \in {Base}_{D} \land 2^{nd} (1^{st} (P)) \in {Base}_{D})) \to (1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Sect (D) 2^{nd} (P))$
95	93 67 89 94	syl12anc	$⊢ (φ \land P \in Sect (C)) \to (1^{st} (1^{st} (P)) Sect (D) 2^{nd} (1^{st} (P)) = 2^{nd} (P) \leftrightarrow ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Sect (D) 2^{nd} (P))$
96	91 95	mpbid	$⊢ (φ \land P \in Sect (C)) \to ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Sect (D) 2^{nd} (P)$
97		df-br	$⊢ ⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩ Sect (D) 2^{nd} (P) \leftrightarrow ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Sect (D)$
98	96 97	sylib	$⊢ (φ \land P \in Sect (C)) \to ⟨⟨1^{st} (1^{st} (P)), 2^{nd} (1^{st} (P))⟩, 2^{nd} (P)⟩ \in Sect (D)$
99	17 98	eqeltrd	$⊢ (φ \land P \in Sect (C)) \to P \in Sect (D)$

Metamath Proof Explorer

Theorem sectpropdlem

Proof