Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gsmhom Unicode version

Definition df-gsmhom 25491
 Description: Define the set of semigroup homomorphisms from to . Experimental. (Contributed by FL, 15-Jul-2012.)
Assertion
Ref Expression
df-gsmhom
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-gsmhom
StepHypRef Expression
1 csmhom 25490 . 2
2 vg . . 3
3 vh . . 3
4 csem 21013 . . 3
52cv 1631 . . . . . . . 8
65cdm 4705 . . . . . . 7
76cdm 4705 . . . . . 6
83cv 1631 . . . . . . . 8
98cdm 4705 . . . . . . 7
109cdm 4705 . . . . . 6
11 vf . . . . . . 7
1211cv 1631 . . . . . 6
137, 10, 12wf 5267 . . . . 5
14 vx . . . . . . . . . . 11
1514cv 1631 . . . . . . . . . 10
1615, 12cfv 5271 . . . . . . . . 9
17 vy . . . . . . . . . . 11
1817cv 1631 . . . . . . . . . 10
1918, 12cfv 5271 . . . . . . . . 9
2016, 19, 8co 5874 . . . . . . . 8
2115, 18, 5co 5874 . . . . . . . . 9
2221, 12cfv 5271 . . . . . . . 8
2320, 22wceq 1632 . . . . . . 7
2423, 17, 7wral 2556 . . . . . 6
2524, 14, 7wral 2556 . . . . 5
2613, 25wa 358 . . . 4
2726, 11cab 2282 . . 3
282, 3, 4, 4, 27cmpt2 5876 . 2
291, 28wceq 1632 1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator