fucsect

Description: Two natural transformations are in a section iff all the components are in a section relation. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	fuciso.q	$⊢ Q = C FuncCat D$
	fuciso.b	$⊢ B = {Base}_{C}$
	fuciso.n	$⊢ N = C Nat D$
	fuciso.f	$⊢ φ \to F \in (C Func D)$
	fuciso.g	$⊢ φ \to G \in (C Func D)$
	fucsect.s	$⊢ S = Sect (Q)$
	fucsect.t	$⊢ T = Sect (D)$
Assertion	fucsect	$⊢ φ \to (U (F S G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x)))$

Proof

Step	Hyp	Ref	Expression
1		fuciso.q	$⊢ Q = C FuncCat D$
2		fuciso.b	$⊢ B = {Base}_{C}$
3		fuciso.n	$⊢ N = C Nat D$
4		fuciso.f	$⊢ φ \to F \in (C Func D)$
5		fuciso.g	$⊢ φ \to G \in (C Func D)$
6		fucsect.s	$⊢ S = Sect (Q)$
7		fucsect.t	$⊢ T = Sect (D)$
8	1	fucbas	$⊢ C Func D = {Base}_{Q}$
9	1 3	fuchom	$⊢ N = Hom (Q)$
10		eqid	$⊢ comp (Q) = comp (Q)$
11		eqid	$⊢ Id (Q) = Id (Q)$
12		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
13	4 12	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
14	13	simpld	$⊢ φ \to C \in Cat$
15	13	simprd	$⊢ φ \to D \in Cat$
16	1 14 15	fuccat	$⊢ φ \to Q \in Cat$
17	8 9 10 11 6 16 4 5	issect	$⊢ φ \to (U (F S G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F)))$
18		ovex	$⊢ V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) \in V$
19	18	rgenw	$⊢ \forall x \in B V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) \in V$
20		mpteqb	$⊢ \forall x \in B V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) \in V \to ((x \in B ⟼ V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x)) = (x \in B ⟼ Id (D) (1^{st} (F) (x))) \leftrightarrow \forall x \in B V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) = Id (D) (1^{st} (F) (x)))$
21	19 20	mp1i	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to ((x \in B ⟼ V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x)) = (x \in B ⟼ Id (D) (1^{st} (F) (x))) \leftrightarrow \forall x \in B V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) = Id (D) (1^{st} (F) (x)))$
22		eqid	$⊢ comp (D) = comp (D)$
23		simprl	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to U \in (F N G)$
24		simprr	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to V \in (G N F)$
25	1 3 2 22 10 23 24	fucco	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to V (⟨F, G⟩ comp (Q) F) U = (x \in B ⟼ V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x))$
26		eqid	$⊢ Id (D) = Id (D)$
27	4	adantr	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to F \in (C Func D)$
28	1 11 26 27	fucid	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to Id (Q) (F) = Id (D) \circ 1^{st} (F)$
29	15	adantr	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to D \in Cat$
30		eqid	$⊢ {Base}_{D} = {Base}_{D}$
31	30 26	cidfn	$⊢ D \in Cat \to Id (D) Fn {Base}_{D}$
32	29 31	syl	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to Id (D) Fn {Base}_{D}$
33		dffn2	$⊢ Id (D) Fn {Base}_{D} \leftrightarrow Id (D) : {Base}_{D} ⟶ V$
34	32 33	sylib	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to Id (D) : {Base}_{D} ⟶ V$
35		relfunc	$⊢ Rel (C Func D)$
36		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
37	35 4 36	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
38	2 30 37	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{D}$
39	38	adantr	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to 1^{st} (F) : B ⟶ {Base}_{D}$
40		fcompt	$⊢ (Id (D) : {Base}_{D} ⟶ V \land 1^{st} (F) : B ⟶ {Base}_{D}) \to Id (D) \circ 1^{st} (F) = (x \in B ⟼ Id (D) (1^{st} (F) (x)))$
41	34 39 40	syl2anc	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to Id (D) \circ 1^{st} (F) = (x \in B ⟼ Id (D) (1^{st} (F) (x)))$
42	28 41	eqtrd	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to Id (Q) (F) = (x \in B ⟼ Id (D) (1^{st} (F) (x)))$
43	25 42	eqeq12d	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to (V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F) \leftrightarrow (x \in B ⟼ V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x)) = (x \in B ⟼ Id (D) (1^{st} (F) (x))))$
44		eqid	$⊢ Hom (D) = Hom (D)$
45	29	adantr	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to D \in Cat$
46	39	ffvelcdmda	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to 1^{st} (F) (x) \in {Base}_{D}$
47		1st2ndbr	$⊢ (Rel (C Func D) \land G \in (C Func D)) \to 1^{st} (G) (C Func D) 2^{nd} (G)$
48	35 5 47	sylancr	$⊢ φ \to 1^{st} (G) (C Func D) 2^{nd} (G)$
49	2 30 48	funcf1	$⊢ φ \to 1^{st} (G) : B ⟶ {Base}_{D}$
50	49	adantr	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to 1^{st} (G) : B ⟶ {Base}_{D}$
51	50	ffvelcdmda	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to 1^{st} (G) (x) \in {Base}_{D}$
52	23	adantr	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to U \in (F N G)$
53	3 52	nat1st2nd	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to U \in (⟨1^{st} (F), 2^{nd} (F)⟩ N ⟨1^{st} (G), 2^{nd} (G)⟩)$
54		simpr	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to x \in B$
55	3 53 2 44 54	natcl	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to U (x) \in (1^{st} (F) (x) Hom (D) 1^{st} (G) (x))$
56	24	adantr	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to V \in (G N F)$
57	3 56	nat1st2nd	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to V \in (⟨1^{st} (G), 2^{nd} (G)⟩ N ⟨1^{st} (F), 2^{nd} (F)⟩)$
58	3 57 2 44 54	natcl	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to V (x) \in (1^{st} (G) (x) Hom (D) 1^{st} (F) (x))$
59	30 44 22 26 7 45 46 51 55 58	issect2	$⊢ ((φ \land (U \in (F N G) \land V \in (G N F))) \land x \in B) \to (U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x) \leftrightarrow V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) = Id (D) (1^{st} (F) (x)))$
60	59	ralbidva	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to (\forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x) \leftrightarrow \forall x \in B V (x) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ comp (D) 1^{st} (F) (x)) U (x) = Id (D) (1^{st} (F) (x)))$
61	21 43 60	3bitr4d	$⊢ (φ \land (U \in (F N G) \land V \in (G N F))) \to (V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F) \leftrightarrow \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x))$
62	61	pm5.32da	$⊢ φ \to (((U \in (F N G) \land V \in (G N F)) \land V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x)))$
63		df-3an	$⊢ (U \in (F N G) \land V \in (G N F) \land V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F))$
64		df-3an	$⊢ (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x)) \leftrightarrow ((U \in (F N G) \land V \in (G N F)) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x))$
65	62 63 64	3bitr4g	$⊢ φ \to ((U \in (F N G) \land V \in (G N F) \land V (⟨F, G⟩ comp (Q) F) U = Id (Q) (F)) \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x)))$
66	17 65	bitrd	$⊢ φ \to (U (F S G) V \leftrightarrow (U \in (F N G) \land V \in (G N F) \land \forall x \in B U (x) (1^{st} (F) (x) T 1^{st} (G) (x)) V (x)))$

Metamath Proof Explorer

Theorem fucsect

Proof