Metamath Proof Explorer

Theorem thincciso4

Description: Two isomorphic categories are either both thin or neither. 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 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincciso4.i ⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )
Assertion thincciso4 ( 𝜑 → ( 𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat ) )

Proof

Step Hyp Ref Expression
1 thincciso2.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 thincciso2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincciso2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
4 thincciso2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 thincciso2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 thincciso4.i ⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 )
7 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
8 1 catccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
9 3 8 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 7 2 9 4 5 cic ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
11 6 10 mpbid ⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) → ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
13 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑈 ∈ 𝑉 )
14 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑋 ∈ 𝐵 )
15 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ 𝐵 )
16 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
17 simplr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑋 ∈ ThinCat )
18 1 2 13 14 15 7 16 17 thincciso3 ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ ThinCat )
19 12 18 exlimddv ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ThinCat ) → 𝑌 ∈ ThinCat )
20 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) → ∃ 𝑓 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
21 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑈 ∈ 𝑉 )
22 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑋 ∈ 𝐵 )
23 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ 𝐵 )
24 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
25 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ ThinCat )
26 1 2 21 22 23 7 24 25 thincciso2 ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) ∧ 𝑓 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑋 ∈ ThinCat )
27 20 26 exlimddv ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ThinCat ) → 𝑋 ∈ ThinCat )
28 19 27 impbida ⊢ ( 𝜑 → ( 𝑋 ∈ ThinCat ↔ 𝑌 ∈ ThinCat ) )