idfullsubc

Description: The source category of an inclusion functor is a full subcategory of the target category if the inclusion functor is full. Remark 4.4(2) in Adamek p. 49. See also ressffth . (Contributed by Zhi Wang, 11-Nov-2025)

	Ref	Expression
Hypotheses	idfth.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
	idsubc.h	⊢ 𝐻 = ( Hom_f ‘ 𝐷 )
	idfullsubc.j	⊢ 𝐽 = ( Hom_f ‘ 𝐸 )
	idfullsubc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	idfullsubc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
Assertion	idfullsubc	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐵 ⊆ 𝐶 ∧ ( 𝐽 ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		idfth.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
2		idsubc.h	⊢ 𝐻 = ( Hom_f ‘ 𝐷 )
3		idfullsubc.j	⊢ 𝐽 = ( Hom_f ‘ 𝐸 )
4		idfullsubc.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
5		idfullsubc.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
6		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
7	6	sseli	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
8	1 7	imaidfu2lem	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )
9	4 8	eqtr4id	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → 𝐵 = ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) )
10		eqid	⊢ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) )
11		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
12		eqid	⊢ ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) )
13		relfull	⊢ Rel ( 𝐷 Full 𝐸 )
14		1st2ndbr	⊢ ( ( Rel ( 𝐷 Full 𝐸 ) ∧ 𝐼 ∈ ( 𝐷 Full 𝐸 ) ) → ( 1^st ‘ 𝐼 ) ( 𝐷 Full 𝐸 ) ( 2^nd ‘ 𝐼 ) )
15	13 14	mpan	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 1^st ‘ 𝐼 ) ( 𝐷 Full 𝐸 ) ( 2^nd ‘ 𝐼 ) )
16	10 11 12 15 5 3	imasubc	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) Fn ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ∧ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ⊆ 𝐶 ∧ ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) ) )
17	16	simp2d	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ⊆ 𝐶 )
18	9 17	eqsstrd	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → 𝐵 ⊆ 𝐶 )
19	16	simp3d	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) )
20	9	sqxpeqd	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐵 × 𝐵 ) = ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) )
21	20	reseq2d	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐽 ↾ ( 𝐵 × 𝐵 ) ) = ( 𝐽 ↾ ( ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) × ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ) ) )
22	1 7 11 2 12 8	imaidfu2	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → 𝐻 = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) )
23	19 21 22	3eqtr4d	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐽 ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 )
24	18 23	jca	⊢ ( 𝐼 ∈ ( 𝐷 Full 𝐸 ) → ( 𝐵 ⊆ 𝐶 ∧ ( 𝐽 ↾ ( 𝐵 × 𝐵 ) ) = 𝐻 ) )

Metamath Proof Explorer

Theorem idfullsubc

Proof