Theorem uobeq3

Description: An isomorphism between categories generates equal sets of universal objects. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobeq2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uobeq2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uobeq2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	uobeq2.g	⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
	uobeq2.y	⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
	uobeq2.q	⊢ 𝑄 = ( CatCat ‘ 𝑈 )
	uobeq3.i	⊢ 𝐼 = ( Iso ‘ 𝑄 )
	uobeq3.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 𝐼 𝐸 ) )
Assertion	uobeq3	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		uobeq2.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		uobeq2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3		uobeq2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4		uobeq2.g	⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
5		uobeq2.y	⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
6		uobeq2.q	⊢ 𝑄 = ( CatCat ‘ 𝑈 )
7		uobeq3.i	⊢ 𝐼 = ( Iso ‘ 𝑄 )
8		uobeq3.1	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 𝐼 𝐸 ) )
9		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
10	6 1 9 7 8	catcisoi	⊢ ( 𝜑 → ( 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ ( 1st ‘ 𝐾 ) : 𝐵 –1-1-onto→ ( Base ‘ 𝐸 ) ) )
11	10	simpld	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
12	1 2 3 4 5 11	uobffth	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )