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 ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
postc.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
postc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
Assertion postc ( 𝜑 → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 → 𝑥 = 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 postc.c ⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2 postc.k ⊢ ( 𝜑 → 𝐾 ∈ Proset )
3 postc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 1 2 prstcprs ⊢ ( 𝜑 → 𝐶 ∈ Proset )
5 eqid ⊢ ( le ‘ 𝐶 ) = ( le ‘ 𝐶 )
6 3 5 ispos2 ⊢ ( 𝐶 ∈ Poset ↔ ( 𝐶 ∈ Proset ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
7 6 baib ⊢ ( 𝐶 ∈ Proset → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
8 4 7 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
9 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐾 ∈ Proset )
11 9 10 prstcthin ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ ThinCat )
12 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
13 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
14 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
15 11 3 12 13 14 thinccic ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ↔ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ≠ ∅ ∧ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ≠ ∅ ) ) )
16 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( le ‘ 𝐶 ) = ( le ‘ 𝐶 ) )
17 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 ) )
18 12 3 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
19 13 3 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
20 9 10 16 17 18 19 prstchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ↔ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ≠ ∅ ) )
21 9 10 16 17 19 18 prstchom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ( le ‘ 𝐶 ) 𝑥 ↔ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ≠ ∅ ) )
22 20 21 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) ↔ ( ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ≠ ∅ ∧ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) ≠ ∅ ) ) )
23 15 22 bitr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 ↔ ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) ) )
24 23 imbi1d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 → 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
25 24 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 ( le ‘ 𝐶 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐶 ) 𝑥 ) → 𝑥 = 𝑦 ) ) )
26 8 25 bitr4d ⊢ ( 𝜑 → ( 𝐶 ∈ Poset ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ≃𝑐 ‘ 𝐶 ) 𝑦 → 𝑥 = 𝑦 ) ) )