Theorem uobeq

Description: If a full functor (in fact, a full embedding) is a section of a functor (surjective on objects), then the sets of universal objects are equal. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	uobffth.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
	uobffth.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	uobffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	uobffth.g	⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
	uobffth.y	⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
	uobeq.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
	uobeq.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
	uobeq.n	⊢ ( 𝜑 → ( 𝐿 ∘func 𝐾 ) = 𝐼 )
	uobeq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐸 Func 𝐷 ) )
Assertion	uobeq	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		uobffth.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		uobffth.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3		uobffth.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4		uobffth.g	⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
5		uobffth.y	⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
6		uobeq.i	⊢ 𝐼 = ( idfunc ‘ 𝐷 )
7		uobeq.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
8		uobeq.n	⊢ ( 𝜑 → ( 𝐿 ∘func 𝐾 ) = 𝐼 )
9		uobeq.l	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐸 Func 𝐷 ) )
10		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
11		fullfunc	⊢ ( 𝐷 Full 𝐸 ) ⊆ ( 𝐷 Func 𝐸 )
12	11 7	sselid	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
13		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝐾 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐾 = ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ )
14	10 12 13	sylancr	⊢ ( 𝜑 → 𝐾 = ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ )
15	12	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐾 ) )
16	9	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) ( 𝐸 Func 𝐷 ) ( 2nd ‘ 𝐿 ) )
17	12 9	cofu1st2nd	⊢ ( 𝜑 → ( 𝐿 ∘func 𝐾 ) = ( ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ) )
18	17 8	eqtr3d	⊢ ( 𝜑 → ( ⟨ ( 1st ‘ 𝐿 ) , ( 2nd ‘ 𝐿 ) ⟩ ∘func ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ) = 𝐼 )
19	6 15 16 18	cofidfth	⊢ ( 𝜑 → ( 1st ‘ 𝐾 ) ( 𝐷 Faith 𝐸 ) ( 2nd ‘ 𝐾 ) )
20		df-br	⊢ ( ( 1st ‘ 𝐾 ) ( 𝐷 Faith 𝐸 ) ( 2nd ‘ 𝐾 ) ↔ ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Faith 𝐸 ) )
21	19 20	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝐾 ) , ( 2nd ‘ 𝐾 ) ⟩ ∈ ( 𝐷 Faith 𝐸 ) )
22	14 21	eqeltrd	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Faith 𝐸 ) )
23	7 22	elind	⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
24	1 2 3 4 5 23	uobffth	⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )