This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setc2obas

Description: (/) and 1o are distinct objects in ( SetCat2o ) . This combined with setc2ohom demonstrates that the category does not have pairwise disjoint hom-sets. See also df-cat and cat1 . (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses setc2ohom.c ⊢ C = SetCat ⁡ 2 𝑜
setc2obas.b ⊢ B = Base C
Assertion setc2obas ⊢ ∅ ∈ B ∧ 1 𝑜 ∈ B ∧ 1 𝑜 ≠ ∅

Proof

Step Hyp Ref Expression
1 setc2ohom.c ⊢ C = SetCat ⁡ 2 𝑜
2 setc2obas.b ⊢ B = Base C
3 0ex ⊢ ∅ ∈ V
4 3 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
5 2oex ⊢ 2 𝑜 ∈ V
6 5 a1i ⊢ ⊤ → 2 𝑜 ∈ V
7 1 6 setcbas ⊢ ⊤ → 2 𝑜 = Base C
8 7 mptru ⊢ 2 𝑜 = Base C
9 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
10 2 8 9 3eqtr2i ⊢ B = ∅ 1 𝑜
11 4 10 eleqtrri ⊢ ∅ ∈ B
12 1oex ⊢ 1 𝑜 ∈ V
13 12 prid2 ⊢ 1 𝑜 ∈ ∅ 1 𝑜
14 13 10 eleqtrri ⊢ 1 𝑜 ∈ B
15 1n0 ⊢ 1 𝑜 ≠ ∅
16 11 14 15 3pm3.2i ⊢ ∅ ∈ B ∧ 1 𝑜 ∈ B ∧ 1 𝑜 ≠ ∅