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

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 ⊢ 𝐵 = ( Base ‘ 𝐷 )
uobeq2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
uobeq2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
uobeq2.g ⊢ ( 𝜑 → ( 𝐾 ∘func 𝐹 ) = 𝐺 )
uobeq2.y ⊢ ( 𝜑 → ( ( 1st ‘ 𝐾 ) ‘ 𝑋 ) = 𝑌 )
uobeq2.q ⊢ 𝑄 = ( CatCat ‘ 𝑈 )
uobeq3.i ⊢ 𝐼 = ( Iso ‘ 𝑄 )
uobeq3.1 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 𝐼 𝐸 ) )
Assertion uobeq3 ( 𝜑 → 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 uobeq3.i ⊢ 𝐼 = ( Iso ‘ 𝑄 )
8 uobeq3.1 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 𝐼 𝐸 ) )
9 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
10 6 1 9 7 8 catcisoi ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ ( 1st ‘ 𝐾 ) : 𝐵 –1-1-onto→ ( Base ‘ 𝐸 ) ) )
11 10 simpld ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
12 1 2 3 4 5 11 uobffth ⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )