Metamath Proof Explorer

Theorem par2hom

Description: The four hom-sets of the explicit two-object parallel-arrow category. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypothesis par2hom.h ⊢ 𝐻 = ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) )
Assertion par2hom ( ( ∅ 𝐻 ∅ ) = { 2o } ∧ ( 1o 𝐻 1o ) = { 2o } ∧ ( ( ∅ 𝐻 1o ) = 2o ∧ ( 1o 𝐻 ∅ ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 par2hom.h ⊢ 𝐻 = ( 𝑚 ∈ 2o , 𝑛 ∈ 2o ↦ if ( 𝑚 = 𝑛 , { 2o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1o ) , 2o , ∅ ) ) )
2 0ex ⊢ ∅ ∈ V
3 2 prid1 ⊢ ∅ ∈ { ∅ , 1o }
4 df2o3 ⊢ 2o = { ∅ , 1o }
5 3 4 eleqtrri ⊢ ∅ ∈ 2o
6 2oex ⊢ 2o ∈ V
7 1 6 parhomval ⊢ ( ( ∅ ∈ 2o ∧ ∅ ∈ 2o ) → ( ∅ 𝐻 ∅ ) = if ( ∅ = ∅ , { 2o } , if ( ( ∅ = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) ) )
8 5 5 7 mp2an ⊢ ( ∅ 𝐻 ∅ ) = if ( ∅ = ∅ , { 2o } , if ( ( ∅ = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) )
9 eqid ⊢ ∅ = ∅
10 9 iftruei ⊢ if ( ∅ = ∅ , { 2o } , if ( ( ∅ = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) ) = { 2o }
11 8 10 eqtri ⊢ ( ∅ 𝐻 ∅ ) = { 2o }
12 1oelpr ⊢ 1o ∈ { ∅ , 1o }
13 12 4 eleqtrri ⊢ 1o ∈ 2o
14 1 6 parhomval ⊢ ( ( 1o ∈ 2o ∧ 1o ∈ 2o ) → ( 1o 𝐻 1o ) = if ( 1o = 1o , { 2o } , if ( ( 1o = ∅ ∧ 1o = 1o ) , 2o , ∅ ) ) )
15 13 13 14 mp2an ⊢ ( 1o 𝐻 1o ) = if ( 1o = 1o , { 2o } , if ( ( 1o = ∅ ∧ 1o = 1o ) , 2o , ∅ ) )
16 eqid ⊢ 1o = 1o
17 16 iftruei ⊢ if ( 1o = 1o , { 2o } , if ( ( 1o = ∅ ∧ 1o = 1o ) , 2o , ∅ ) ) = { 2o }
18 15 17 eqtri ⊢ ( 1o 𝐻 1o ) = { 2o }
19 1 6 parhomval ⊢ ( ( ∅ ∈ 2o ∧ 1o ∈ 2o ) → ( ∅ 𝐻 1o ) = if ( ∅ = 1o , { 2o } , if ( ( ∅ = ∅ ∧ 1o = 1o ) , 2o , ∅ ) ) )
20 5 13 19 mp2an ⊢ ( ∅ 𝐻 1o ) = if ( ∅ = 1o , { 2o } , if ( ( ∅ = ∅ ∧ 1o = 1o ) , 2o , ∅ ) )
21 1n0 ⊢ 1o ≠ ∅
22 21 nesymi ⊢ ¬ ∅ = 1o
23 22 iffalsei ⊢ if ( ∅ = 1o , { 2o } , if ( ( ∅ = ∅ ∧ 1o = 1o ) , 2o , ∅ ) ) = if ( ( ∅ = ∅ ∧ 1o = 1o ) , 2o , ∅ )
24 9 16 pm3.2i ⊢ ( ∅ = ∅ ∧ 1o = 1o )
25 24 iftruei ⊢ if ( ( ∅ = ∅ ∧ 1o = 1o ) , 2o , ∅ ) = 2o
26 20 23 25 3eqtri ⊢ ( ∅ 𝐻 1o ) = 2o
27 1 6 parhomval ⊢ ( ( 1o ∈ 2o ∧ ∅ ∈ 2o ) → ( 1o 𝐻 ∅ ) = if ( 1o = ∅ , { 2o } , if ( ( 1o = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) ) )
28 13 5 27 mp2an ⊢ ( 1o 𝐻 ∅ ) = if ( 1o = ∅ , { 2o } , if ( ( 1o = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) )
29 21 neii ⊢ ¬ 1o = ∅
30 29 iffalsei ⊢ if ( 1o = ∅ , { 2o } , if ( ( 1o = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) ) = if ( ( 1o = ∅ ∧ ∅ = 1o ) , 2o , ∅ )
31 29 intnanr ⊢ ¬ ( 1o = ∅ ∧ ∅ = 1o )
32 31 iffalsei ⊢ if ( ( 1o = ∅ ∧ ∅ = 1o ) , 2o , ∅ ) = ∅
33 28 30 32 3eqtri ⊢ ( 1o 𝐻 ∅ ) = ∅
34 26 33 pm3.2i ⊢ ( ( ∅ 𝐻 1o ) = 2o ∧ ( 1o 𝐻 ∅ ) = ∅ )
35 11 18 34 3pm3.2i ⊢ ( ( ∅ 𝐻 ∅ ) = { 2o } ∧ ( 1o 𝐻 1o ) = { 2o } ∧ ( ( ∅ 𝐻 1o ) = 2o ∧ ( 1o 𝐻 ∅ ) = ∅ ) )