This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐸 ) 𝑌 ) )