Metamath Proof Explorer

Theorem par2catid

Description: A concrete category with two objects and two parallel nonidentity arrows. The two identity arrows both have raw value 2o ; their sources and targets distinguish them. The parallel arrows have raw values the empty set and 1o . (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypothesis par2catid.c ⊢ C = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
Assertion par2catid ⊢ C ∈ Cat ∧ Id ⁡ C = y ∈ 2 𝑜 ⟼ 2 𝑜

Proof

Step Hyp Ref Expression
1 par2catid.c ⊢ C = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
2 2oex ⊢ 2 𝑜 ∈ V
3 2on ⊢ 2 𝑜 ∈ On
4 ontr ⊢ 2 𝑜 ∈ On → Tr ⁡ 2 𝑜
5 3 4 ax-mp ⊢ Tr ⁡ 2 𝑜
6 dftr4 ⊢ Tr ⁡ 2 𝑜 ↔ 2 𝑜 ⊆ 𝒫 2 𝑜
7 5 6 mpbi ⊢ 2 𝑜 ⊆ 𝒫 2 𝑜
8 df-3o ⊢ 3 𝑜 = suc ⁡ 2 𝑜
9 df-suc ⊢ suc ⁡ 2 𝑜 = 2 𝑜 ∪ 2 𝑜
10 8 9 eqtri ⊢ 3 𝑜 = 2 𝑜 ∪ 2 𝑜
11 eqid ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅
12 eqid ⊢ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s = r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
13 eqid ⊢ p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s = p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
14 2 2 7 10 11 12 13 1 parcatid ⊢ C ∈ Cat ∧ Id ⁡ C = y ∈ 2 𝑜 ⟼ 2 𝑜