This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Zhi Wang Examples of categories Thin categories thincciso3
Description: Categories isomorphic to a thin category are thin. Example 3.26(2)
of Adamek p. 33. Note that "thincciso2.u" is redundant thanks to
elbasfv . (Contributed by Zhi Wang , 18-Oct-2025)
Ref
Expression
Hypotheses
thincciso2.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
thincciso2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincciso2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
thincciso2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincciso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincciso2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
thincciso2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
thincciso3.xt ⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
Assertion
thincciso3 ⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
Proof
Step
Hyp
Ref
Expression
1
thincciso2.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2
thincciso2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3
thincciso2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4
thincciso2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5
thincciso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6
thincciso2.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
7
thincciso2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8
thincciso3.xt ⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
9
eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
10
1
catccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
11
3 10
syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
12
2 9 11 4 5 6
invf ⊢ ( 𝜑 → ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) : ( 𝑋 𝐼 𝑌 ) ⟶ ( 𝑌 𝐼 𝑋 ) )
13
12 7
ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ‘ 𝐹 ) ∈ ( 𝑌 𝐼 𝑋 ) )
14
1 2 3 5 4 6 13 8
thincciso2 ⊢ ( 𝜑 → 𝑌 ∈ ThinCat )