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 ⊢ B = Base D
uobffth.x ⊢ φ → X ∈ B
uobffth.f ⊢ φ → F ∈ C Func D
uobffth.g ⊢ φ → K ∘ func F = G
uobffth.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
uobeq.i ⊢ I = id func ⁡ D
uobeq.k ⊢ φ → K ∈ D Full E
uobeq.n ⊢ φ → L ∘ func K = I
uobeq.l ⊢ φ → L ∈ E Func D
Assertion uobeq Could not format assertion : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 uobffth.b ⊢ B = Base D
2 uobffth.x ⊢ φ → X ∈ B
3 uobffth.f ⊢ φ → F ∈ C Func D
4 uobffth.g ⊢ φ → K ∘ func F = G
5 uobffth.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
6 uobeq.i ⊢ I = id func ⁡ D
7 uobeq.k ⊢ φ → K ∈ D Full E
8 uobeq.n ⊢ φ → L ∘ func K = I
9 uobeq.l ⊢ φ → L ∈ E Func D
10 relfunc ⊢ Rel ⁡ D Func E
11 fullfunc ⊢ D Full E ⊆ D Func E
12 11 7 sselid ⊢ φ → K ∈ D Func E
13 1st2nd ⊢ Rel ⁡ D Func E ∧ K ∈ D Func E → K = 1 st ⁡ K 2 nd ⁡ K
14 10 12 13 sylancr ⊢ φ → K = 1 st ⁡ K 2 nd ⁡ K
15 12 func1st2nd ⊢ φ → 1 st ⁡ K D Func E 2 nd ⁡ K
16 9 func1st2nd ⊢ φ → 1 st ⁡ L E Func D 2 nd ⁡ L
17 12 9 cofu1st2nd ⊢ φ → L ∘ func K = 1 st ⁡ L 2 nd ⁡ L ∘ func 1 st ⁡ K 2 nd ⁡ K
18 17 8 eqtr3d ⊢ φ → 1 st ⁡ L 2 nd ⁡ L ∘ func 1 st ⁡ K 2 nd ⁡ K = I
19 6 15 16 18 cofidfth ⊢ φ → 1 st ⁡ K D Faith E 2 nd ⁡ K
20 df-br ⊢ 1 st ⁡ K D Faith E 2 nd ⁡ K ↔ 1 st ⁡ K 2 nd ⁡ K ∈ D Faith E
21 19 20 sylib ⊢ φ → 1 st ⁡ K 2 nd ⁡ K ∈ D Faith E
22 14 21 eqeltrd ⊢ φ → K ∈ D Faith E
23 7 22 elind ⊢ φ → K ∈ D Full E ∩ D Faith E
24 1 2 3 4 5 23 uobffth Could not format ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ph -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-