thinccisod

Description: Two thin categories are isomorphic if the induced preorders are order-isomorphic (deduction form). Example 3.26(2) of Adamek p. 33. (Contributed by Zhi Wang, 22-Sep-2025)

	Ref	Expression
Hypotheses	thinccisod.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
	thinccisod.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
	thinccisod.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
	thinccisod.h	⊢ 𝐻 = ( Hom ‘ 𝑋 )
	thinccisod.j	⊢ 𝐽 = ( Hom ‘ 𝑌 )
	thinccisod.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	thinccisod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	thinccisod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
	thinccisod.xt	⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
	thinccisod.yt	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
	thinccisod.f	⊢ ( 𝜑 → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
	thinccisod.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
Assertion	thinccisod	⊢ ( 𝜑 → 𝑋 ( ≃_𝑐 ‘ 𝐶 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		thinccisod.c	⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2		thinccisod.r	⊢ 𝑅 = ( Base ‘ 𝑋 )
3		thinccisod.s	⊢ 𝑆 = ( Base ‘ 𝑌 )
4		thinccisod.h	⊢ 𝐻 = ( Hom ‘ 𝑋 )
5		thinccisod.j	⊢ 𝐽 = ( Hom ‘ 𝑌 )
6		thinccisod.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
7		thinccisod.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
8		thinccisod.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
9		thinccisod.xt	⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
10		thinccisod.yt	⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
11		thinccisod.f	⊢ ( 𝜑 → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
12		thinccisod.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
13		f1of	⊢ ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 → 𝐹 : 𝑅 ⟶ 𝑆 )
14	11 13	syl	⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ 𝑆 )
15		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑋 ) ∈ V )
16	2 15	eqeltrid	⊢ ( 𝜑 → 𝑅 ∈ V )
17	14 16	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
18	12	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
19	18 11	jca	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ∧ 𝐹 : 𝑅 –1-1-onto→ 𝑆 ) )
20		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
21		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
22	20 21	oveq12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) )
23	22	eqeq1d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) )
24	23	bibi2d	⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
25	24	2ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ) )
26		f1oeq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝑅 –1-1-onto→ 𝑆 ↔ 𝐹 : 𝑅 –1-1-onto→ 𝑆 ) )
27	25 26	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝐹 ‘ 𝑥 ) 𝐽 ( 𝐹 ‘ 𝑦 ) ) = ∅ ) ∧ 𝐹 : 𝑅 –1-1-onto→ 𝑆 ) ) )
28	17 19 27	spcedv	⊢ ( 𝜑 → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) )
29		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
30	9	thinccd	⊢ ( 𝜑 → 𝑋 ∈ Cat )
31	7 30	elind	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Cat ) )
32	1 29 6	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( 𝑈 ∩ Cat ) )
33	31 32	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
34	10	thinccd	⊢ ( 𝜑 → 𝑌 ∈ Cat )
35	8 34	elind	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑈 ∩ Cat ) )
36	35 32	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐶 ) )
37	1 29 2 3 4 5 6 33 36 9 10	thincciso	⊢ ( 𝜑 → ( 𝑋 ( ≃_𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) )
38	28 37	mpbird	⊢ ( 𝜑 → 𝑋 ( ≃_𝑐 ‘ 𝐶 ) 𝑌 )

Metamath Proof Explorer

Theorem thinccisod

Proof