Theorem catcisoi

Description: A functor is an isomorphism of categories only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in Adamek p. 34. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	catcisoi.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	catcisoi.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
	catcisoi.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
	catcisoi.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
	catcisoi.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
Assertion	catcisoi	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		catcisoi.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		catcisoi.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
3		catcisoi.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
4		catcisoi.i	⊢ 𝐼 = ( Iso ‘ 𝐶 )
5		catcisoi.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
6		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7	4 5 6	isorcl2	⊢ ( 𝜑 → ( 𝑋 ∈ ( Base ‘ 𝐶 ) ∧ 𝑌 ∈ ( Base ‘ 𝐶 ) ) )
8	7	simpld	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
9	1 6	elbasfv	⊢ ( 𝑋 ∈ ( Base ‘ 𝐶 ) → 𝑈 ∈ V )
10	8 9	syl	⊢ ( 𝜑 → 𝑈 ∈ V )
11	7	simprd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
12	1 6 2 3 10 8 11 4	catciso	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) ↔ ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
13	5 12	mpbid	⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝐹 ) : 𝑅 –1-1-onto→ 𝑆 ) )