cofull

Description: The composition of two full functors is full. Proposition 3.30(d) in Adamek p. 35. (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	cofull.f	$⊢ φ \to F \in (C Full D)$
	cofull.g	$⊢ φ \to G \in (D Full E)$
Assertion	cofull	$⊢ φ \to G \circ_{func} F \in (C Full E)$

Proof

Step	Hyp	Ref	Expression
1		cofull.f	$⊢ φ \to F \in (C Full D)$
2		cofull.g	$⊢ φ \to G \in (D Full E)$
3		relfunc	$⊢ Rel (C Func E)$
4		fullfunc	$⊢ C Full D \subseteq C Func D$
5	4 1	sseldi	$⊢ φ \to F \in (C Func D)$
6		fullfunc	$⊢ D Full E \subseteq D Func E$
7	6 2	sseldi	$⊢ φ \to G \in (D Func E)$
8	5 7	cofucl	$⊢ φ \to G \circ_{func} F \in (C Func E)$
9		1st2nd	$⊢ (Rel (C Func E) \land G \circ_{func} F \in (C Func E)) \to G \circ_{func} F = ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩$
10	3 8 9	sylancr	$⊢ φ \to G \circ_{func} F = ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩$
11		1st2ndbr	$⊢ (Rel (C Func E) \land G \circ_{func} F \in (C Func E)) \to 1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F)$
12	3 8 11	sylancr	$⊢ φ \to 1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F)$
13		eqid	$⊢ {Base}_{D} = {Base}_{D}$
14		eqid	$⊢ Hom (E) = Hom (E)$
15		eqid	$⊢ Hom (D) = Hom (D)$
16		relfull	$⊢ Rel (D Full E)$
17	2	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to G \in (D Full E)$
18		1st2ndbr	$⊢ (Rel (D Full E) \land G \in (D Full E)) \to 1^{st} (G) (D Full E) 2^{nd} (G)$
19	16 17 18	sylancr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G) (D Full E) 2^{nd} (G)$
20		eqid	$⊢ {Base}_{C} = {Base}_{C}$
21		relfunc	$⊢ Rel (C Func D)$
22	5	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F \in (C Func D)$
23		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
24	21 22 23	sylancr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
25	20 13 24	funcf1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
26		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
27	25 26	ffvelrnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (x) \in {Base}_{D}$
28		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
29	25 28	ffvelrnd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (y) \in {Base}_{D}$
30	13 14 15 19 27 29	fullfo	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) \underset{onto}{⟶} 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
31		eqid	$⊢ Hom (C) = Hom (C)$
32		relfull	$⊢ Rel (C Full D)$
33	1	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to F \in (C Full D)$
34		1st2ndbr	$⊢ (Rel (C Full D) \land F \in (C Full D)) \to 1^{st} (F) (C Full D) 2^{nd} (F)$
35	32 33 34	sylancr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (C Full D) 2^{nd} (F)$
36	20 15 31 35 26 28	fullfo	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
37		foco	$⊢ ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) : 1^{st} (F) (x) Hom (D) 1^{st} (F) (y) \underset{onto}{⟶} 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)) \land (x 2^{nd} (F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)) \to ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
38	30 36 37	syl2anc	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
39	7	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to G \in (D Func E)$
40	20 22 39 26 28	cofu2nd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (G \circ_{func} F) y = (1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)$
41		eqidd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x Hom (C) y = x Hom (C) y$
42	20 22 39 26	cofu1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (x) = 1^{st} (G) (1^{st} (F) (x))$
43	20 22 39 28	cofu1	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (y) = 1^{st} (G) (1^{st} (F) (y))$
44	42 43	oveq12d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y) = 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y))$
45	40 41 44	foeq123d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to ((x 2^{nd} (G \circ_{func} F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y) \leftrightarrow ((1^{st} (F) (x) 2^{nd} (G) 1^{st} (F) (y)) \circ (x 2^{nd} (F) y)) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G) (1^{st} (F) (x)) Hom (E) 1^{st} (G) (1^{st} (F) (y)))$
46	38 45	mpbird	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (G \circ_{func} F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y)$
47	46	ralrimivva	$⊢ φ \to \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (G \circ_{func} F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y)$
48	20 14 31	isfull2	$⊢ 1^{st} (G \circ_{func} F) (C Full E) 2^{nd} (G \circ_{func} F) \leftrightarrow (1^{st} (G \circ_{func} F) (C Func E) 2^{nd} (G \circ_{func} F) \land \forall x \in {Base}_{C} \forall y \in {Base}_{C} (x 2^{nd} (G \circ_{func} F) y) : x Hom (C) y \underset{onto}{⟶} 1^{st} (G \circ_{func} F) (x) Hom (E) 1^{st} (G \circ_{func} F) (y))$
49	12 47 48	sylanbrc	$⊢ φ \to 1^{st} (G \circ_{func} F) (C Full E) 2^{nd} (G \circ_{func} F)$
50		df-br	$⊢ 1^{st} (G \circ_{func} F) (C Full E) 2^{nd} (G \circ_{func} F) \leftrightarrow ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩ \in (C Full E)$
51	49 50	sylib	$⊢ φ \to ⟨1^{st} (G \circ_{func} F), 2^{nd} (G \circ_{func} F)⟩ \in (C Full E)$
52	10 51	eqeltrd	$⊢ φ \to G \circ_{func} F \in (C Full E)$

Metamath Proof Explorer

Theorem cofull

Proof