Metamath Proof Explorer

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 ⊢ 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
uobeq3.i ⊢ I = Iso ⁡ Q
uobeq3.1 ⊢ φ → K ∈ D I E
Assertion uobeq3 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 uobeq3.i ⊢ I = Iso ⁡ Q
8 uobeq3.1 ⊢ φ → K ∈ D I E
9 eqid ⊢ Sect ⁡ Q = Sect ⁡ Q
10 eqid ⊢ Base E = Base E
11 6 1 10 7 8 catcisoi ⊢ φ → K ∈ D Full E ∩ D Faith E ∧ 1 st ⁡ K : B ⟶ 1-1 onto Base E
12 11 simpld ⊢ φ → K ∈ D Full E ∩ D Faith E
13 12 elin1d ⊢ φ → K ∈ D Full E
14 eqid ⊢ Inv ⁡ Q = Inv ⁡ Q
15 14 7 isoval2 ⊢ D I E = dom ⁡ D Inv ⁡ Q E
16 8 15 eleqtrdi ⊢ φ → K ∈ dom ⁡ D Inv ⁡ Q E
17 eldmg ⊢ K ∈ dom ⁡ D Inv ⁡ Q E → K ∈ dom ⁡ D Inv ⁡ Q E ↔ ∃ l K D Inv ⁡ Q E l
18 17 ibi ⊢ K ∈ dom ⁡ D Inv ⁡ Q E → ∃ l K D Inv ⁡ Q E l
19 14 9 isinv2 ⊢ K D Inv ⁡ Q E l ↔ K D Sect ⁡ Q E l ∧ l E Sect ⁡ Q D K
20 19 simplbi ⊢ K D Inv ⁡ Q E l → K D Sect ⁡ Q E l
21 20 eximi ⊢ ∃ l K D Inv ⁡ Q E l → ∃ l K D Sect ⁡ Q E l
22 16 18 21 3syl ⊢ φ → ∃ l K D Sect ⁡ Q E l
23 eldmg ⊢ K ∈ D I E → K ∈ dom ⁡ D Sect ⁡ Q E ↔ ∃ l K D Sect ⁡ Q E l
24 8 23 syl ⊢ φ → K ∈ dom ⁡ D Sect ⁡ Q E ↔ ∃ l K D Sect ⁡ Q E l
25 22 24 mpbird ⊢ φ → K ∈ dom ⁡ D Sect ⁡ Q E
26 1 2 3 4 5 6 9 13 25 uobeq2 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 |-