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 ⊢ ( Sect ‘ 𝑄 ) = ( Sect ‘ 𝑄 )
10 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11 6 1 10 7 8 catcisoi ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) ∧ ( 1st ‘ 𝐾 ) : 𝐵 –1-1-onto→ ( Base ‘ 𝐸 ) ) )
12 11 simpld ⊢ ( 𝜑 → 𝐾 ∈ ( ( 𝐷 Full 𝐸 ) ∩ ( 𝐷 Faith 𝐸 ) ) )
13 12 elin1d ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Full 𝐸 ) )
14 eqid ⊢ ( Inv ‘ 𝑄 ) = ( Inv ‘ 𝑄 )
15 14 7 isoval2 ⊢ ( 𝐷 𝐼 𝐸 ) = dom ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 )
16 8 15 eleqtrdi ⊢ ( 𝜑 → 𝐾 ∈ dom ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) )
17 eldmg ⊢ ( 𝐾 ∈ dom ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) → ( 𝐾 ∈ dom ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) ↔ ∃ 𝑙 𝐾 ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) 𝑙 ) )
18 17 ibi ⊢ ( 𝐾 ∈ dom ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) → ∃ 𝑙 𝐾 ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) 𝑙 )
19 14 9 isinv2 ⊢ ( 𝐾 ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) 𝑙 ↔ ( 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 ∧ 𝑙 ( 𝐸 ( Sect ‘ 𝑄 ) 𝐷 ) 𝐾 ) )
20 19 simplbi ⊢ ( 𝐾 ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) 𝑙 → 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 )
21 20 eximi ⊢ ( ∃ 𝑙 𝐾 ( 𝐷 ( Inv ‘ 𝑄 ) 𝐸 ) 𝑙 → ∃ 𝑙 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 )
22 16 18 21 3syl ⊢ ( 𝜑 → ∃ 𝑙 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 )
23 eldmg ⊢ ( 𝐾 ∈ ( 𝐷 𝐼 𝐸 ) → ( 𝐾 ∈ dom ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) ↔ ∃ 𝑙 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 ) )
24 8 23 syl ⊢ ( 𝜑 → ( 𝐾 ∈ dom ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) ↔ ∃ 𝑙 𝐾 ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) 𝑙 ) )
25 22 24 mpbird ⊢ ( 𝜑 → 𝐾 ∈ dom ( 𝐷 ( Sect ‘ 𝑄 ) 𝐸 ) )
26 1 2 3 4 5 6 9 13 25 uobeq2 ⊢ ( 𝜑 → dom ( 𝐹 ( 𝐶 UP 𝐷 ) 𝑋 ) = dom ( 𝐺 ( 𝐶 UP 𝐸 ) 𝑌 ) )