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 
|- H = ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) )
Assertion par2hom 
|- ( ( (/) H (/) ) = { 2o } /\ ( 1o H 1o ) = { 2o } /\ ( ( (/) H 1o ) = 2o /\ ( 1o H (/) ) = (/) ) )

Proof

Step Hyp Ref Expression
1 par2hom.h 
 |-  H = ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) )
2 0ex 
 |-  (/) e. _V
3 2 prid1 
 |-  (/) e. { (/) , 1o }
4 df2o3 
 |-  2o = { (/) , 1o }
5 3 4 eleqtrri 
 |-  (/) e. 2o
6 2oex 
 |-  2o e. _V
7 1 6 parhomval 
 |-  ( ( (/) e. 2o /\ (/) e. 2o ) -> ( (/) H (/) ) = if ( (/) = (/) , { 2o } , if ( ( (/) = (/) /\ (/) = 1o ) , 2o , (/) ) ) )
8 5 5 7 mp2an 
 |-  ( (/) H (/) ) = if ( (/) = (/) , { 2o } , if ( ( (/) = (/) /\ (/) = 1o ) , 2o , (/) ) )
9 eqid 
 |-  (/) = (/)
10 9 iftruei 
 |-  if ( (/) = (/) , { 2o } , if ( ( (/) = (/) /\ (/) = 1o ) , 2o , (/) ) ) = { 2o }
11 8 10 eqtri 
 |-  ( (/) H (/) ) = { 2o }
12 1oelpr 
 |-  1o e. { (/) , 1o }
13 12 4 eleqtrri 
 |-  1o e. 2o
14 1 6 parhomval 
 |-  ( ( 1o e. 2o /\ 1o e. 2o ) -> ( 1o H 1o ) = if ( 1o = 1o , { 2o } , if ( ( 1o = (/) /\ 1o = 1o ) , 2o , (/) ) ) )
15 13 13 14 mp2an 
 |-  ( 1o H 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 H 1o ) = { 2o }
19 1 6 parhomval 
 |-  ( ( (/) e. 2o /\ 1o e. 2o ) -> ( (/) H 1o ) = if ( (/) = 1o , { 2o } , if ( ( (/) = (/) /\ 1o = 1o ) , 2o , (/) ) ) )
20 5 13 19 mp2an 
 |-  ( (/) H 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 
 |-  ( (/) H 1o ) = 2o
27 1 6 parhomval 
 |-  ( ( 1o e. 2o /\ (/) e. 2o ) -> ( 1o H (/) ) = if ( 1o = (/) , { 2o } , if ( ( 1o = (/) /\ (/) = 1o ) , 2o , (/) ) ) )
28 13 5 27 mp2an 
 |-  ( 1o H (/) ) = 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 H (/) ) = (/)
34 26 33 pm3.2i 
 |-  ( ( (/) H 1o ) = 2o /\ ( 1o H (/) ) = (/) )
35 11 18 34 3pm3.2i 
 |-  ( ( (/) H (/) ) = { 2o } /\ ( 1o H 1o ) = { 2o } /\ ( ( (/) H 1o ) = 2o /\ ( 1o H (/) ) = (/) ) )