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

Metamath Proof Explorer

Theorem uobeq2

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

Ref Expression
Hypotheses uobeq2.b ⊢ B = Base D
uobeq2.x ⊢ φ → X ∈ B
uobeq2.f ⊢ φ → F ∈ C Func D
uobeq2.g ⊢ φ → K ∘ func F = G
uobeq2.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
uobeq2.q ⊢ Q = CatCat ⁡ U
uobeq2.s ⊢ S = Sect ⁡ Q
uobeq2.k ⊢ φ → K ∈ D Full E
uobeq2.1 ⊢ φ → K ∈ dom ⁡ D S E
Assertion uobeq2 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 uobeq2.b ⊢ B = Base D
2 uobeq2.x ⊢ φ → X ∈ B
3 uobeq2.f ⊢ φ → F ∈ C Func D
4 uobeq2.g ⊢ φ → K ∘ func F = G
5 uobeq2.y ⊢ φ → 1 st ⁡ K ⁡ X = Y
6 uobeq2.q ⊢ Q = CatCat ⁡ U
7 uobeq2.s ⊢ S = Sect ⁡ Q
8 uobeq2.k ⊢ φ → K ∈ D Full E
9 uobeq2.1 ⊢ φ → K ∈ dom ⁡ D S E
10 eldmg ⊢ K ∈ dom ⁡ D S E → K ∈ dom ⁡ D S E ↔ ∃ l K D S E l
11 10 ibi ⊢ K ∈ dom ⁡ D S E → ∃ l K D S E l
12 9 11 syl ⊢ φ → ∃ l K D S E l
13 2 adantr ⊢ φ ∧ K D S E l → X ∈ B
14 3 adantr ⊢ φ ∧ K D S E l → F ∈ C Func D
15 4 adantr ⊢ φ ∧ K D S E l → K ∘ func F = G
16 5 adantr ⊢ φ ∧ K D S E l → 1 st ⁡ K ⁡ X = Y
17 eqid ⊢ id func ⁡ D = id func ⁡ D
18 8 adantr ⊢ φ ∧ K D S E l → K ∈ D Full E
19 eqid ⊢ Hom ⁡ Q = Hom ⁡ Q
20 6 19 17 7 catcsect ⊢ K D S E l ↔ K ∈ D Hom ⁡ Q E ∧ l ∈ E Hom ⁡ Q D ∧ l ∘ func K = id func ⁡ D
21 20 simprbi ⊢ K D S E l → l ∘ func K = id func ⁡ D
22 21 adantl ⊢ φ ∧ K D S E l → l ∘ func K = id func ⁡ D
23 20 simplbi ⊢ K D S E l → K ∈ D Hom ⁡ Q E ∧ l ∈ E Hom ⁡ Q D
24 23 simprd ⊢ K D S E l → l ∈ E Hom ⁡ Q D
25 6 19 24 elcatchom ⊢ K D S E l → l ∈ E Func D
26 25 adantl ⊢ φ ∧ K D S E l → l ∈ E Func D
27 1 13 14 15 16 17 18 22 26 uobeq Could not format ( ( ph /\ K ( D S E ) l ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) : No typesetting found for |- ( ( ph /\ K ( D S E ) l ) -> dom ( F ( C UP D ) X ) = dom ( G ( C UP E ) Y ) ) with typecode |-
28 12 27 exlimddv 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 |-