Metamath Proof Explorer

Theorem postc

Description: The converted category is a poset iff no distinct objects are isomorphic. (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses postc.c ⊢ φ → C = ProsetToCat ⁡ K
postc.k ⊢ φ → K ∈ Proset
postc.b ⊢ B = Base C
Assertion postc ⊢ φ → C ∈ Poset ↔ ∀ x ∈ B ∀ y ∈ B x ≃ 𝑐 ⁡ C y → x = y

Proof

Step Hyp Ref Expression
1 postc.c ⊢ φ → C = ProsetToCat ⁡ K
2 postc.k ⊢ φ → K ∈ Proset
3 postc.b ⊢ B = Base C
4 1 2 prstcprs ⊢ φ → C ∈ Proset
5 eqid ⊢ ≤ C = ≤ C
6 3 5 ispos2 ⊢ C ∈ Poset ↔ C ∈ Proset ∧ ∀ x ∈ B ∀ y ∈ B x ≤ C y ∧ y ≤ C x → x = y
7 6 baib ⊢ C ∈ Proset → C ∈ Poset ↔ ∀ x ∈ B ∀ y ∈ B x ≤ C y ∧ y ≤ C x → x = y
8 4 7 syl ⊢ φ → C ∈ Poset ↔ ∀ x ∈ B ∀ y ∈ B x ≤ C y ∧ y ≤ C x → x = y
9 1 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B → C = ProsetToCat ⁡ K
10 2 adantr ⊢ φ ∧ x ∈ B ∧ y ∈ B → K ∈ Proset
11 9 10 prstcthin ⊢ φ ∧ x ∈ B ∧ y ∈ B → C ∈ ThinCat
12 simprl ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ B
13 simprr ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ B
14 eqid ⊢ Hom ⁡ C = Hom ⁡ C
15 11 3 12 13 14 thinccic ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≃ 𝑐 ⁡ C y ↔ x Hom ⁡ C y ≠ ∅ ∧ y Hom ⁡ C x ≠ ∅
16 eqidd ⊢ φ ∧ x ∈ B ∧ y ∈ B → ≤ C = ≤ C
17 eqidd ⊢ φ ∧ x ∈ B ∧ y ∈ B → Hom ⁡ C = Hom ⁡ C
18 12 3 eleqtrdi ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ∈ Base C
19 13 3 eleqtrdi ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ∈ Base C
20 9 10 16 17 18 19 prstchom ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≤ C y ↔ x Hom ⁡ C y ≠ ∅
21 9 10 16 17 19 18 prstchom ⊢ φ ∧ x ∈ B ∧ y ∈ B → y ≤ C x ↔ y Hom ⁡ C x ≠ ∅
22 20 21 anbi12d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≤ C y ∧ y ≤ C x ↔ x Hom ⁡ C y ≠ ∅ ∧ y Hom ⁡ C x ≠ ∅
23 15 22 bitr4d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≃ 𝑐 ⁡ C y ↔ x ≤ C y ∧ y ≤ C x
24 23 imbi1d ⊢ φ ∧ x ∈ B ∧ y ∈ B → x ≃ 𝑐 ⁡ C y → x = y ↔ x ≤ C y ∧ y ≤ C x → x = y
25 24 2ralbidva ⊢ φ → ∀ x ∈ B ∀ y ∈ B x ≃ 𝑐 ⁡ C y → x = y ↔ ∀ x ∈ B ∀ y ∈ B x ≤ C y ∧ y ≤ C x → x = y
26 8 25 bitr4d ⊢ φ → C ∈ Poset ↔ ∀ x ∈ B ∀ y ∈ B x ≃ 𝑐 ⁡ C y → x = y