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 No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
postc.k ⊢φ→K∈Proset
postc.b ⊢B=BaseC
Assertion postc ⊢φ→C∈Poset↔∀x∈B∀y∈Bx≃𝑐⁡Cy→x=y

Proof

Step Hyp Ref Expression
1 postc.c Could not format ( ph -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ph -> C = ( ProsetToCat ` K ) ) with typecode |-
2 postc.k ⊢φ→K∈Proset
3 postc.b ⊢B=BaseC
4 1 2 prstcprs ⊢φ→C∈Proset
5 eqid ⊢≤C=≤C
6 3 5 ispos2 ⊢C∈Poset↔C∈Proset∧∀x∈B∀y∈Bx≤Cy∧y≤Cx→x=y
7 6 baib ⊢C∈Proset→C∈Poset↔∀x∈B∀y∈Bx≤Cy∧y≤Cx→x=y
8 4 7 syl ⊢φ→C∈Poset↔∀x∈B∀y∈Bx≤Cy∧y≤Cx→x=y
9 1 adantr Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> C = ( ProsetToCat ` K ) ) : No typesetting found for |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C = ( ProsetToCat ` K ) ) with typecode |-
10 2 adantr ⊢φ∧x∈B∧y∈B→K∈Proset
11 9 10 prstcthin Could not format ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> C e. ThinCat ) with typecode |-
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≃𝑐⁡Cy↔xHom⁡Cy≠∅∧yHom⁡Cx≠∅
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∈BaseC
19 13 3 eleqtrdi ⊢φ∧x∈B∧y∈B→y∈BaseC
20 9 10 16 17 18 19 prstchom ⊢φ∧x∈B∧y∈B→x≤Cy↔xHom⁡Cy≠∅
21 9 10 16 17 19 18 prstchom ⊢φ∧x∈B∧y∈B→y≤Cx↔yHom⁡Cx≠∅
22 20 21 anbi12d ⊢φ∧x∈B∧y∈B→x≤Cy∧y≤Cx↔xHom⁡Cy≠∅∧yHom⁡Cx≠∅
23 15 22 bitr4d ⊢φ∧x∈B∧y∈B→x≃𝑐⁡Cy↔x≤Cy∧y≤Cx
24 23 imbi1d ⊢φ∧x∈B∧y∈B→x≃𝑐⁡Cy→x=y↔x≤Cy∧y≤Cx→x=y
25 24 2ralbidva ⊢φ→∀x∈B∀y∈Bx≃𝑐⁡Cy→x=y↔∀x∈B∀y∈Bx≤Cy∧y≤Cx→x=y
26 8 25 bitr4d ⊢φ→C∈Poset↔∀x∈B∀y∈Bx≃𝑐⁡Cy→x=y