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 ⊢ 𝐵 = ( Base ‘ 𝐷 )
uobeq2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
uobeq2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
uobeq2.g ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
uobeq2.y ⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
uobeq2.q ⊢ 𝑄 = ( CatCat ‘ 𝑈 )
uobeq2.s ⊢ 𝑆 = ( Sect ‘ 𝑄 )
uobeq2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
uobeq2.1 ⊢ ( 𝜑 → 𝐾 ∈ dom ( 𝐷 𝑆 𝐸 ) )
Assertion uobeq2 ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )

Proof

Step Hyp Ref Expression
1 uobeq2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
2 uobeq2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
3 uobeq2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
4 uobeq2.g ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
5 uobeq2.y ⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
6 uobeq2.q ⊢ 𝑄 = ( CatCat ‘ 𝑈 )
7 uobeq2.s ⊢ 𝑆 = ( Sect ‘ 𝑄 )
8 uobeq2.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
9 uobeq2.1 ⊢ ( 𝜑 → 𝐾 ∈ dom ( 𝐷 𝑆 𝐸 ) )
10 eldmg ⊢ ( 𝐾 ∈ dom ( 𝐷 𝑆 𝐸 ) → ( 𝐾 ∈ dom ( 𝐷 𝑆 𝐸 ) ↔ ∃ 𝑙 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) )
11 10 ibi ⊢ ( 𝐾 ∈ dom ( 𝐷 𝑆 𝐸 ) → ∃ 𝑙 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 )
12 9 11 syl ⊢ ( 𝜑 → ∃ 𝑙 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 )
13 eqid ⊢ ( idfunc ‘ 𝐷 ) = ( idfunc ‘ 𝐷 )
14 2 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → 𝑋 ∈ 𝐵 )
15 3 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
18 5 adantr ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
19 eqid ⊢ ( Hom ‘ 𝑄 ) = ( Hom ‘ 𝑄 )
20 6 19 13 7 catcsect ⊢ ( 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ↔ ( ( 𝐾 ∈ ( 𝐷 ( Hom ‘ 𝑄 ) 𝐸 ) ∧ 𝑙 ∈ ( 𝐸 ( Hom ‘ 𝑄 ) 𝐷 ) ) ∧ ( 𝑙 ∘func 𝐾 ) = ( idfunc ‘ 𝐷 ) ) )
21 20 simprbi ⊢ ( 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 → ( 𝑙 ∘func 𝐾 ) = ( idfunc ‘ 𝐷 ) )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → ( 𝑙 ∘func 𝐾 ) = ( idfunc ‘ 𝐷 ) )
23 20 simplbi ⊢ ( 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 → ( 𝐾 ∈ ( 𝐷 ( Hom ‘ 𝑄 ) 𝐸 ) ∧ 𝑙 ∈ ( 𝐸 ( Hom ‘ 𝑄 ) 𝐷 ) ) )
24 23 simprd ⊢ ( 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 → 𝑙 ∈ ( 𝐸 ( Hom ‘ 𝑄 ) 𝐷 ) )
25 6 19 24 elcatchom ⊢ ( 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 → 𝑙 ∈ ( 𝐸 Func 𝐷 ) )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → 𝑙 ∈ ( 𝐸 Func 𝐷 ) )
27 1 13 14 15 16 17 18 22 26 uobeq ⊢ ( ( 𝜑 ∧ 𝐾 ( 𝐷 𝑆 𝐸 ) 𝑙 ) → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )
28 12 27 exlimddv ⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )