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	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
	cofull.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Full 𝐸 ) )
Assertion	cofull	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Full 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		cofull.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
2		cofull.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Full 𝐸 ) )
3		relfunc	⊢ Rel ( 𝐶 Func 𝐸 )
4		fullfunc	⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
5	4 1	sselid	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
6		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
7	6 2	sselid	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
8	5 7	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
9		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) ) → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ )
10	3 8 9	sylancr	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) = ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ )
11		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) ) → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) )
12	3 8 11	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) )
13		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
14		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
15		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
16		relfull	⊢ Rel ( 𝐷 Full 𝐸 )
17	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐷 Full 𝐸 ) )
18		1st2ndbr	⊢ ( ( Rel ( 𝐷 Full 𝐸 ) ∧ 𝐺 ∈ ( 𝐷 Full 𝐸 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Full 𝐸 ) ( 2^nd ‘ 𝐺 ) )
19	16 17 18	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐺 ) ( 𝐷 Full 𝐸 ) ( 2^nd ‘ 𝐺 ) )
20		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
21		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
22	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
23		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
24	21 22 23	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
25	20 13 24	funcf1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
26		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27	25 26	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
28		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
29	25 28	ffvelrnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
30	13 14 15 19 27 29	fullfo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) –onto→ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
31		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
32		relfull	⊢ Rel ( 𝐶 Full 𝐷 )
33	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐹 ∈ ( 𝐶 Full 𝐷 ) )
34		1st2ndbr	⊢ ( ( Rel ( 𝐶 Full 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Full 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2^nd ‘ 𝐹 ) )
35	32 33 34	sylancr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Full 𝐷 ) ( 2^nd ‘ 𝐹 ) )
36	20 15 31 35 26 28	fullfo	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
37		foco	⊢ ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) –onto→ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ∧ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
38	30 36 37	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
39	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
40	20 22 39 26 28	cofu2nd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
41		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
42	20 22 39 26	cofu1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
43	20 22 39 28	cofu1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) = ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
44	42 43	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) )
45	40 41 44	foeq123d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ↔ ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝐺 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ 𝐺 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) ) ) )
46	38 45	mpbird	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) )
47	46	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) )
48	20 14 31	isfull2	⊢ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Full 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ↔ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) –onto→ ( ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑥 ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ‘ 𝑦 ) ) ) )
49	12 47 48	sylanbrc	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Full 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) )
50		df-br	⊢ ( ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) ( 𝐶 Full 𝐸 ) ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ↔ ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ ∈ ( 𝐶 Full 𝐸 ) )
51	49 50	sylib	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 𝐺 ∘_func 𝐹 ) ) , ( 2^nd ‘ ( 𝐺 ∘_func 𝐹 ) ) ⟩ ∈ ( 𝐶 Full 𝐸 ) )
52	10 51	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ∘_func 𝐹 ) ∈ ( 𝐶 Full 𝐸 ) )

Metamath Proof Explorer

Theorem cofull

Proof