Metamath Proof Explorer

Theorem thincciso

Description: Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of Adamek p. 33. (Contributed by Zhi Wang, 16-Oct-2024)

Ref Expression
Hypotheses thincciso.c ⊢ C = CatCat ⁡ U
thincciso.b ⊢ B = Base C
thincciso.r ⊢ R = Base X
thincciso.s ⊢ S = Base Y
thincciso.h ⊢ H = Hom ⁡ X
thincciso.j ⊢ J = Hom ⁡ Y
thincciso.u ⊢ φ → U ∈ V
thincciso.x ⊢ φ → X ∈ B
thincciso.y ⊢ φ → Y ∈ B
thincciso.xt No typesetting found for |- ( ph -> X e. ThinCat ) with typecode |-
thincciso.yt No typesetting found for |- ( ph -> Y e. ThinCat ) with typecode |-
Assertion thincciso ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S

Proof

Step Hyp Ref Expression
1 thincciso.c ⊢ C = CatCat ⁡ U
2 thincciso.b ⊢ B = Base C
3 thincciso.r ⊢ R = Base X
4 thincciso.s ⊢ S = Base Y
5 thincciso.h ⊢ H = Hom ⁡ X
6 thincciso.j ⊢ J = Hom ⁡ Y
7 thincciso.u ⊢ φ → U ∈ V
8 thincciso.x ⊢ φ → X ∈ B
9 thincciso.y ⊢ φ → Y ∈ B
10 thincciso.xt Could not format ( ph -> X e. ThinCat ) : No typesetting found for |- ( ph -> X e. ThinCat ) with typecode |-
11 thincciso.yt Could not format ( ph -> Y e. ThinCat ) : No typesetting found for |- ( ph -> Y e. ThinCat ) with typecode |-
12 eqid ⊢ Iso ⁡ C = Iso ⁡ C
13 1 catccat ⊢ U ∈ V → C ∈ Cat
14 7 13 syl ⊢ φ → C ∈ Cat
15 12 2 14 8 9 cic ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ ∃ a a ∈ X Iso ⁡ C Y
16 opex ⊢ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ V
17 16 a1i ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ V
18 biimp ⊢ x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ → x H y = ∅ → f ⁡ x J f ⁡ y = ∅
19 18 2ralimi ⊢ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ → ∀ x ∈ R ∀ y ∈ R x H y = ∅ → f ⁡ x J f ⁡ y = ∅
20 19 ad2antrl ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → ∀ x ∈ R ∀ y ∈ R x H y = ∅ → f ⁡ x J f ⁡ y = ∅
21 11 adantr Could not format ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> Y e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> Y e. ThinCat ) with typecode |-
22 eqid ⊢ z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w = z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w
23 10 adantr Could not format ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> X e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( A. x e. R A. y e. R ( ( x H y ) = (/) <-> ( ( f ` x ) J ( f ` y ) ) = (/) ) /\ f : R -1-1-onto-> S ) ) -> X e. ThinCat ) with typecode |-
24 23 thinccd ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → X ∈ Cat
25 simprr ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f : R ⟶ 1-1 onto S
26 f1of ⊢ f : R ⟶ 1-1 onto S → f : R ⟶ S
27 25 26 syl ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f : R ⟶ S
28 biimpr ⊢ x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ → f ⁡ x J f ⁡ y = ∅ → x H y = ∅
29 28 2ralimi ⊢ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ → ∀ x ∈ R ∀ y ∈ R f ⁡ x J f ⁡ y = ∅ → x H y = ∅
30 29 ad2antrl ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → ∀ x ∈ R ∀ y ∈ R f ⁡ x J f ⁡ y = ∅ → x H y = ∅
31 3 4 5 6 24 21 27 22 30 functhinc ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f X Func Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ↔ z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w = z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w
32 22 31 mpbiri ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f X Func Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w
33 3 6 5 21 32 fullthinc ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f X Full Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ↔ ∀ x ∈ R ∀ y ∈ R x H y = ∅ → f ⁡ x J f ⁡ y = ∅
34 20 33 mpbird ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f X Full Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w
35 df-br ⊢ f X Full Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ↔ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y
36 34 35 sylib ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y
37 23 32 thincfth ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f X Faith Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w
38 df-br ⊢ f X Faith Y z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ↔ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Faith Y
39 37 38 sylib ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Faith Y
40 36 39 elind ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y ∩ X Faith Y
41 vex ⊢ f ∈ V
42 3 fvexi ⊢ R ∈ V
43 42 42 mpoex ⊢ z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ V
44 41 43 op1st ⊢ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w = f
45 f1oeq1 ⊢ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w = f → 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S ↔ f : R ⟶ 1-1 onto S
46 44 45 ax-mp ⊢ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S ↔ f : R ⟶ 1-1 onto S
47 25 46 sylibr ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S
48 40 47 jca ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y ∩ X Faith Y ∧ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S
49 1 2 3 4 7 8 9 12 catciso ⊢ φ → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Iso ⁡ C Y ↔ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y ∩ X Faith Y ∧ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S
50 49 biimpar ⊢ φ ∧ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Full Y ∩ X Faith Y ∧ 1 st ⁡ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Iso ⁡ C Y
51 48 50 syldan ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Iso ⁡ C Y
52 eleq1 ⊢ a = f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w → a ∈ X Iso ⁡ C Y ↔ f z ∈ R , w ∈ R ⟼ z H w × f ⁡ z J f ⁡ w ∈ X Iso ⁡ C Y
53 17 51 52 spcedv ⊢ φ ∧ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → ∃ a a ∈ X Iso ⁡ C Y
54 53 ex ⊢ φ → ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → ∃ a a ∈ X Iso ⁡ C Y
55 54 exlimdv ⊢ φ → ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S → ∃ a a ∈ X Iso ⁡ C Y
56 fvexd ⊢ φ ∧ a ∈ X Iso ⁡ C Y → 1 st ⁡ a ∈ V
57 relfull ⊢ Rel ⁡ X Full Y
58 1 2 3 4 7 8 9 12 catciso ⊢ φ → a ∈ X Iso ⁡ C Y ↔ a ∈ X Full Y ∩ X Faith Y ∧ 1 st ⁡ a : R ⟶ 1-1 onto S
59 58 biimpa ⊢ φ ∧ a ∈ X Iso ⁡ C Y → a ∈ X Full Y ∩ X Faith Y ∧ 1 st ⁡ a : R ⟶ 1-1 onto S
60 59 simpld ⊢ φ ∧ a ∈ X Iso ⁡ C Y → a ∈ X Full Y ∩ X Faith Y
61 60 elin1d ⊢ φ ∧ a ∈ X Iso ⁡ C Y → a ∈ X Full Y
62 1st2ndbr ⊢ Rel ⁡ X Full Y ∧ a ∈ X Full Y → 1 st ⁡ a X Full Y 2 nd ⁡ a
63 57 61 62 sylancr ⊢ φ ∧ a ∈ X Iso ⁡ C Y → 1 st ⁡ a X Full Y 2 nd ⁡ a
64 11 adantr Could not format ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> Y e. ThinCat ) : No typesetting found for |- ( ( ph /\ a e. ( X ( Iso ` C ) Y ) ) -> Y e. ThinCat ) with typecode |-
65 fullfunc ⊢ X Full Y ⊆ X Func Y
66 65 ssbri ⊢ 1 st ⁡ a X Full Y 2 nd ⁡ a → 1 st ⁡ a X Func Y 2 nd ⁡ a
67 63 66 syl ⊢ φ ∧ a ∈ X Iso ⁡ C Y → 1 st ⁡ a X Func Y 2 nd ⁡ a
68 3 6 5 64 67 fullthinc ⊢ φ ∧ a ∈ X Iso ⁡ C Y → 1 st ⁡ a X Full Y 2 nd ⁡ a ↔ ∀ x ∈ R ∀ y ∈ R x H y = ∅ → 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
69 63 68 mpbid ⊢ φ ∧ a ∈ X Iso ⁡ C Y → ∀ x ∈ R ∀ y ∈ R x H y = ∅ → 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
70 67 adantr ⊢ φ ∧ a ∈ X Iso ⁡ C Y ∧ x ∈ R ∧ y ∈ R → 1 st ⁡ a X Func Y 2 nd ⁡ a
71 simprl ⊢ φ ∧ a ∈ X Iso ⁡ C Y ∧ x ∈ R ∧ y ∈ R → x ∈ R
72 simprr ⊢ φ ∧ a ∈ X Iso ⁡ C Y ∧ x ∈ R ∧ y ∈ R → y ∈ R
73 3 5 6 70 71 72 funcf2 ⊢ φ ∧ a ∈ X Iso ⁡ C Y ∧ x ∈ R ∧ y ∈ R → x 2 nd ⁡ a y : x H y ⟶ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y
74 73 f002 ⊢ φ ∧ a ∈ X Iso ⁡ C Y ∧ x ∈ R ∧ y ∈ R → 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ → x H y = ∅
75 74 ralrimivva ⊢ φ ∧ a ∈ X Iso ⁡ C Y → ∀ x ∈ R ∀ y ∈ R 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ → x H y = ∅
76 2ralbiim ⊢ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ ↔ ∀ x ∈ R ∀ y ∈ R x H y = ∅ → 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ ∧ ∀ x ∈ R ∀ y ∈ R 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ → x H y = ∅
77 69 75 76 sylanbrc ⊢ φ ∧ a ∈ X Iso ⁡ C Y → ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
78 59 simprd ⊢ φ ∧ a ∈ X Iso ⁡ C Y → 1 st ⁡ a : R ⟶ 1-1 onto S
79 77 78 jca ⊢ φ ∧ a ∈ X Iso ⁡ C Y → ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ ∧ 1 st ⁡ a : R ⟶ 1-1 onto S
80 fveq1 ⊢ f = 1 st ⁡ a → f ⁡ x = 1 st ⁡ a ⁡ x
81 fveq1 ⊢ f = 1 st ⁡ a → f ⁡ y = 1 st ⁡ a ⁡ y
82 80 81 oveq12d ⊢ f = 1 st ⁡ a → f ⁡ x J f ⁡ y = 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y
83 82 eqeq1d ⊢ f = 1 st ⁡ a → f ⁡ x J f ⁡ y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
84 83 bibi2d ⊢ f = 1 st ⁡ a → x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ↔ x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
85 84 2ralbidv ⊢ f = 1 st ⁡ a → ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ↔ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅
86 f1oeq1 ⊢ f = 1 st ⁡ a → f : R ⟶ 1-1 onto S ↔ 1 st ⁡ a : R ⟶ 1-1 onto S
87 85 86 anbi12d ⊢ f = 1 st ⁡ a → ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S ↔ ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ 1 st ⁡ a ⁡ x J 1 st ⁡ a ⁡ y = ∅ ∧ 1 st ⁡ a : R ⟶ 1-1 onto S
88 56 79 87 spcedv ⊢ φ ∧ a ∈ X Iso ⁡ C Y → ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S
89 88 ex ⊢ φ → a ∈ X Iso ⁡ C Y → ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S
90 89 exlimdv ⊢ φ → ∃ a a ∈ X Iso ⁡ C Y → ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S
91 55 90 impbid ⊢ φ → ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S ↔ ∃ a a ∈ X Iso ⁡ C Y
92 15 91 bitr4d ⊢ φ → X ≃ 𝑐 ⁡ C Y ↔ ∃ f ∀ x ∈ R ∀ y ∈ R x H y = ∅ ↔ f ⁡ x J f ⁡ y = ∅ ∧ f : R ⟶ 1-1 onto S