idsubc

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

	Ref	Expression
Hypotheses	idfth.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
	idsubc.h	⊢ 𝐻 = ( Hom_f ‘ 𝐷 )
Assertion	idsubc	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐻 ∈ ( Subcat ‘ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		idfth.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
2		idsubc.h	⊢ 𝐻 = ( Hom_f ‘ 𝐷 )
3		id	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐼 ∈ ( 𝐷 Func 𝐸 ) )
4		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
5		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 ‘ 𝐷 ) ‘ 𝑝 ) ) )
6	1 3	imaidfu2lem	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝐷 ) )
7	1 3 4 2 5 6	imaidfu2	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐻 = ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) )
8		eqid	⊢ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) = ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) )
9	3	func1st2nd	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( 1^st ‘ 𝐼 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝐼 ) )
10		f1oi	⊢ ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 )
11		dff1o3	⊢ ( ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –1-1-onto→ ( Base ‘ 𝐷 ) ↔ ( ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –onto→ ( Base ‘ 𝐷 ) ∧ Fun ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
12	10 11	mpbi	⊢ ( ( I ↾ ( Base ‘ 𝐷 ) ) : ( Base ‘ 𝐷 ) –onto→ ( Base ‘ 𝐷 ) ∧ Fun ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) )
13	12	simpri	⊢ Fun ^◡ ( I ↾ ( Base ‘ 𝐷 ) )
14		eqidd	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 ) )
15	1 3 14	idfu1sta	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( 1^st ‘ 𝐼 ) = ( I ↾ ( Base ‘ 𝐷 ) ) )
16	15	cnveqd	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ^◡ ( 1^st ‘ 𝐼 ) = ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) )
17	16	funeqd	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( Fun ^◡ ( 1^st ‘ 𝐼 ) ↔ Fun ^◡ ( I ↾ ( Base ‘ 𝐷 ) ) ) )
18	13 17	mpbiri	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → Fun ^◡ ( 1^st ‘ 𝐼 ) )
19	8 4 5 9 18	imasubc3	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → ( 𝑥 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) , 𝑦 ∈ ( ( 1^st ‘ 𝐼 ) “ ( Base ‘ 𝐷 ) ) ↦ ∪ 𝑝 ∈ ( ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑥 } ) × ( ^◡ ( 1^st ‘ 𝐼 ) “ { 𝑦 } ) ) ( ( ( 2^nd ‘ 𝐼 ) ‘ 𝑝 ) “ ( ( Hom ‘ 𝐷 ) ‘ 𝑝 ) ) ) ∈ ( Subcat ‘ 𝐸 ) )
20	7 19	eqeltrd	⊢ ( 𝐼 ∈ ( 𝐷 Func 𝐸 ) → 𝐻 ∈ ( Subcat ‘ 𝐸 ) )

Metamath Proof Explorer

Theorem idsubc

Proof